Section LF. Variable prop:Set. Variable imp: prop -> prop -> prop. Infix NONA 7 "=>" imp. Variable T: prop -> Set. Variable impI : (a,b:prop) ((T a) -> (T b)) -> (T(a => b)). Variable impE : (a,b:prop) (T(a => b)) -> (T a) -> (T b). Lemma trans: (a,b,c:prop) (T(a=>b))->(T(b=>c))->(T(a=>c)). Intros a b c. Intros hab hbc. Apply impI. Intro ha. Apply impE with b. Exact hbc. (* Assumption *) Apply impE with a. Exact hab. (* Assumption *) Exact ha. (* Assumption *) Qed. Lemma exa : (a,b,c:prop) (T((a=>b)=>((b=>c)=>(a=>c)))). Abort. Lemma exb :(a,b,c:prop) (T(((a=>b)=>c)=>(b=>c))). Abort. Variable conj: prop -> prop -> prop. Infix NONA 8 "X" conj. (* Define yourself conjI *) Variable conjI : (a,b:prop) (T a) -> (T b) -> (T(a X b)). Variable conjE1 : (a,b:prop) (T(a X b)) -> (T a). Variable conjE2 : (a,b:prop) (T(a X b)) -> (T b). Lemma weak : (a,b,c:prop)(T((a=>c))) -> (T((a X b) => c)). Intros a b c. Intro Hac. Apply impI. Intro hab. Apply impE with a. Assumption. Apply conjE1 with b. Assumption. Qed. Lemma exc: (a,b,c:prop)(T((a=>b))) -> (T (a=>c)) -> (T(a => (b X c))). Abort. Variable bot:prop. Definition not [a:prop]:= (a=>bot). Variable botE : (a:prop) (T bot)-> (T a). Variable class : (a:prop) (T(not(not a))) -> (T a). Lemma pierce :(a,b:prop) (T(((a=>b)=>a)=>a)). Proof. Intros a b. Apply impI;Intro h. Apply class. Unfold not;Apply impI. Intro na. Apply impE with a; Try Assumption. Apply impE with a=>b; Try Assumption. Apply impI. Intro ha. Apply botE. Apply impE with a;Assumption. Qed. Lemma exd : (a,b:prop)(T(a=>b)) -> (T(a=>(not b))) -> (T(not a)). Abort. Lemma exe : (a,b,c:prop)(T(a=>b)X(a=>(not b))) -> (T(a=>c)). Abort. (* Now predicate logic over a domain D, with constant d, unary function f and one binary relation R *) Variable D: Set. Variable d: D. Variable f: D->D. Variable R: D -> D->prop. Variable fall : (D->prop)->prop. Variable fallI :(P: D->prop)((x:D)(T(P x))) -> (T(fall P)). Variable fallE : (P: D->prop)(T(fall P))->(x:D)(T(P x)). (* We prove (forall z:D (forall x,y:D (R x y)) -> (R z z)) *) (* Hint: first write down the natural deduction *) Lemma triv: (T (fall [z:D] ((fall[x:D] (fall[y:D](R x y)))) => (R z z))). Proof. Apply fallI. Intro z. Apply impI. Intro H. Generalize (fallE [x:D](fall [y:D](R x y)) H). Intro H1. Generalize (H1 z). Intro H2. Generalize (fallE [y:D](R z y) H2). Intro H3. Exact (H3 z). Qed. Lemma triv': (T (fall [z:D] ((fall[x:D] (fall[y:D](R x y)))) => (R z z))). Proof. Apply fallI. Intro z. Apply impI. Intro H. Generalize (fallE ? H). Intro H1. Generalize (H1 z). Intro H2. Generalize (fallE ? H2). Intro H3. Auto. Qed. Lemma triv'': (T (fall [z:D] ((fall[x:D] (fall[y:D](R x y)))) => (R z z))). Proof. Apply fallI. Intro z. Apply impI. Intro H. LetTac H1 := (fallE [x:D](fall [y:D](R x y)) H). LetTac H2 := (H1 z). LetTac H3:= (fallE [y:D](R z y) H2). Exact (H3 z). Qed. (* Exercise: Try using LetTac or using Generalize *) Lemma ASimpIR: (T( (fall [x:D](fall [y:D] ((R x y)=>bot))) => (fall [z:D] ((R z z)=> bot)))). Abort. End LF. (* Lambda calculus *) Section LambdaCalc. Variable L : Set. Variable app : L->L->L. Variable abs : (L->L)->L. Definition Id := (abs [x:L]x). Definition Kcomb := (abs [x:L](abs [y:L]x)). (* Exercise: Define Scomb = \xyz.xz(yz) and omega =\x.xx *) (* Definition Scomb := *) (* Definition omega := *) Variable beq: L->L->Set. Infix NONA 7 "<=>" beq. Variable brefl :(x:L) (x <=> x). Variable bsym :(x,y:L) (x <=> y) -> (y<=>x). Variable btrans :(x,y,z:L) (x <=> y) -> (y<=>z) -> (x<=>z). Variable mon :(x,x',z,z':L) (x<=> x')->(z<=> z')->(app z x)<=>(app z' x'). Variable xi :(f,g:L->L)((x:L)(f x)<=>(g x)) ->(abs f)<=>(abs g). Variable beta :(f:L->L;x:L)(app(abs f)x)<=>(f x). Lemma iden : (x:L)(app Id x) <=> x. Proof. Intro x. Apply (beta [z:L]z). Qed. Lemma exf : (x,y:L)(app (abs [z:L]y) x) <=> (app Id y). Abort. End LambdaCalc.