Section LF.
Variable prop:Set.
Variable imp: prop -> prop -> prop. 

Infix NONA 7 "=>" imp.
(*
Syntax constr level 7:
  imp_infix [(imp $_ $e1 $e2)] ->
    [[<hov 1> $e1:E [0 1] "[=>]" $e2:L]].*)


Variable T: prop -> Prop.
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)))).
Intros a b c.
Apply impI.
Intro hab. 
Apply impI. 
Intro hbc.
Apply impI.
Intro ha.
Apply impE with b.
Exact hbc. (* Assumption *)
Apply impE with a.
Exact hab. (* Assumption *)
Exact ha. (* Assumption *)
Qed.

Lemma exb :(a,b,c:prop) (T(((a=>b)=>c)=>(b=>c))).
Intros a b c.
Apply impI.
Intro habc.
Apply impI.
Intro hb.
Apply impE with (a=>b).
Exact habc.
Apply impI.
Intro ha; Exact hb.
Qed.

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))).
Intros a b c hab hac.
Apply impI.
Intro ha.
Apply conjI.
Apply (impE ?? hab); Exact ha. 
Apply (impE ?? hac); Exact ha. 
Qed.

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 exd : (a,b:prop)(T(a=>b)) -> (T(a=>(not b))) -> (T(not a)).
Intros a b hab hanb.
Unfold not.
Apply impI.
Abort.


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.

(* 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: *)
Lemma ASimpIR: (T( (fall [x:D](fall [y:D] ((R x y)=>bot)))
	=> (fall [z:D] ((R z z)=> bot)))).
Proof.
Apply impI.
Intro AS.
Apply fallI.
Intro z.
Apply impI.
Intro H.
LetTac H1 := (fallE ? AS z).
LetTac H2 := (fallE ? H1 z).
EApply impE. 
Apply H2.
Exact H.
Qed.

Lemma ASimpIR': (T( (fall [x:D](fall [y:D] ((R x y)=>bot)))
	=> (fall [z:D] ((R z z)=> bot)))).
Proof.
Apply impI.
Intro AS.
Apply fallI.
Intro z.
Apply impI.
Intro H.
LetTac H1 := (fallE ? AS z).
LetTac H2 := (fallE ? H1 z).
LetTac H3 := (impE ?? H2).
Apply H3.
Exact H.
Qed.

End LF.

(* Lambda calculus *)
Section LambdaCalc.
Variable L : Set.
Variable app : L->L->L. 
Variable abs : (L->L)->L. 

(* Exercise: Define Scomb and omega *)
Definition Id := (abs [x:L]x).
Definition Kcomb := (abs [x:L](abs [y:L]x)).
Definition Scomb := (abs [x:L](abs [y:L] (abs [z:L](app (app x z)(app y z))))).
Definition omega := (abs [x:L](app x x)).

Variable beq: L->L->Prop. 

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 exe : (x,y:L)(app (abs [z:L]y) x) <=> (app Id y).
Intros x y.
Generalize (beta [_:L]y x).
Intro H.
Apply btrans with y.
Exact H.
Apply bsym.
Exact (iden y).
Qed.

End LambdaCalc.