Intro Lean 3

Posted on August 2, 2019
Tags: lean

inductive CrazyType : blah -> helo -> ResultantType

inductive blehType : A -> B -> C
#C is the Resultant type of blehType.
inductive C : 
#check Sort 
  OUTPUT> Prop :: Type
#check Sort 0  
  OUTPUT> Prop :: Type
#check Sort 1
  OUTPUT> Type :: Type 1

1 Syntax sugar

Below is how to construct type and a b

# sugared but will error
inductive and (a b : Prop) : Prop
| intro : a → b → and a b
# unsugared but notice we omit `a b` in `and a b`
inductive and (a b : Prop) : Prop
| intro : a → b → and

2 logical system

namespace logical_symbols

inductive and (a b : Prop) : Prop
| intro : a → b → and
--sugar for, a -> b -> and a b
--says if you have a proof of 'a' and a proof of 'b' then
--you can build a proof of 'and a b'



inductive or (a b : Prop) : Prop
| intro_left  : a → or
| intro_right : b → or

inductive imply ( a b : Prop) : Prop 
| intro: (a -> b) -> imply

inductive iff (a b : Prop) : Prop
| intro : (a → b) → (b → a) → iff

inductive Exists {α : Type} (p : α → Prop) : Prop
| intro : ∀a : α, p a → Exists

inductive true : Prop
| intro : true

inductive false : Prop

inductive eq {α : Type} : α → α → Prop
| refl : ∀a : α, eq a a
constants P Q : Prop
constant x : P 
constant y : Q
#check and.intro x y :: and P Q
#check and P Q :: Prop

#check P -> P :: Prop
#check imply P P :: Prop
--original lean version
example : P -> P :=
λ (x:P), x

--our custom designed version
example : imply P P :=
imply.intro (λ (x:P), x)

Notice we just designed the lean proof system. The constructor imply.intro builds the term aka proof for it’s associated inductive type below

inductive imply ( a b : Prop) : Prop 
| intro: (a -> b) -> imply

3 Layers of types

Bool and Props are not the same.

There are 2 layers for Props
The 1st layer is designing well-formed Proposition.
The 2nd layer is designing proofs of those Propositions.

layer 1

-------------------------
    true :: Prop

layer 2

-------------------------
   true.intro :: True

In layer 1 we build a tree of well-formed propositions which may or may not be provable through the inductive type definitions .

inductive and (a b : Prop) : Prop
..
inductive or (a b : Prop) : Prop
..
inductive imply ( a b : Prop) : Prop 
..
inductive iff (a b : Prop) : Prop
..
inductive Exists {α : Type} (p : α → Prop) : Prop
..
inductive true : Prop
..
inductive false : Prop
 P    P    True
  \  /     /
   and   /
     \  /
     imply

imply (and P P) True :: Prop

In layer 2 we build a tree of proof of the proposition using the term constructors of the inductive types.

# Desugared term constructor `imply` to `imply a b`

inductive imply ( a b : Prop) : Prop 
| intro: (a -> b) -> imply a b

inductive true : Prop
| intro : true

Goal is to build a term for `imply (and P P) true`

example : imply (and P P) :=
imply.intro (λ(x:and P P), true.intro)


      λ (x:and P P), true.intro :: (a -> b)
   ----------------------------------------
          imply.intro :: imply a b

\[\cfrac{\cfrac{\square::\mathbb{N} \qquad \square::\mathbb{N}}{\square::Score} \qquad\cfrac{\square::\mathbb{N} \qquad \square::\mathbb{N}}{\square::Score} }{step \square \square :: Prop}\]

But also notice we have to check each type to make sure the chain of types terminate eg.

\[Score :: ... :: Type\]

big::ADJ   guy::N  
 -------------           
   \     /        
subj big guy::S   hunts::V
        \            /
  -------------------------
    big guy hunts::SENTENCE

4 

Tree is Type formation aka designing a wellformed proposition
Imp (And P Q) (And P P) :: Prop 

     Imp
    /  \
  And  And
 /  \   /  \
P   Q   P   P

Below is term introduction aka creating a proof. The lambda term below has type 
Imp (And P Q) (And P P)

λ (x:And P Q), And.intro (x.right:P) (x.right:P)

\[\cfrac{\cfrac{[P \land Q]^x}{P^{x.right}} \qquad \cfrac{[P \land Q]^x}{P^{x.right}}}{P \land P^{And.intro}}\]