From 8fa6a59d37eafaea6b21450efd679081bd83bcba Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Wed, 20 Apr 2011 08:49:15 +0000
Subject: [PATCH] generatin lemmas and subject reduction (with a lot of
 axioms).

---
 matita/matita/lib/lambda/inversion.ma |  95 ++++++++++
 matita/matita/lib/lambda/subject.ma   | 263 ++++++++++++++++++++++++++
 2 files changed, 358 insertions(+)
 create mode 100644 matita/matita/lib/lambda/inversion.ma
 create mode 100644 matita/matita/lib/lambda/subject.ma

diff --git a/matita/matita/lib/lambda/inversion.ma b/matita/matita/lib/lambda/inversion.ma
new file mode 100644
index 000000000..b25b315e3
--- /dev/null
+++ b/matita/matita/lib/lambda/inversion.ma
@@ -0,0 +1,95 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "lambda/types.ma".
+
+(*
+inductive TJ: list T → T → T → Prop ≝
+  | ax : ∀i,j. A i j → TJ (nil T) (Sort i) (Sort j)
+  | start: ∀G.∀A.∀i.TJ G A (Sort i) → TJ (A::G) (Rel 0) (lift A 0 1)
+  | weak: ∀G.∀A,B,C.∀i.
+     TJ G A B → TJ G C (Sort i) → TJ (C::G) (lift A 0 1) (lift B 0 1)
+  | prod: ∀G.∀A,B.∀i,j,k. R i j k →
+     TJ G A (Sort i) → TJ (A::G) B (Sort j) → TJ G (Prod A B) (Sort k)
+  | app: ∀G.∀F,A,B,a. 
+     TJ G F (Prod A B) → TJ G a A → TJ G (App F a) (subst B 0 a)
+  | abs: ∀G.∀A,B,b.∀i. 
+     TJ (A::G) b B → TJ G (Prod A B) (Sort i) → TJ G (Lambda A b) (Prod A B)
+  | conv: ∀G.∀A,B,C.∀i. conv B C →
+     TJ G A B → TJ G C (Sort i) → TJ G A C
+  | dummy: ∀G.∀A,B.∀i. 
+     TJ G A B → TJ G B (Sort i) → TJ G (D A) B.
+     axiom prod_inv : ∀G,M,P,Q. G ⊢ M : Prod P Q →
+ ∃i. P::G ⊢ Q : Sort i. *)
+
+axiom lambda_lift : ∀A,B,C. lift A 0 1 = Lambda B C →
+∃P,Q. A = Lambda P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
+
+axiom prod_lift : ∀A,B,C. lift A 0 1 = Prod B C →
+∃P,Q. A = Prod P Q ∧ lift P 0 1  = B ∧ lift Q 1 1 = C.
+
+axiom conv_lift: ∀M,N. conv M N → conv (lift M 0 1) (lift N 0 1).
+ 
+axiom weak_in: ∀G.∀A,B,M,N.∀i.A::G  ⊢ M : N → G ⊢ B : Sort i → 
+ (lift A 0 1)::B::G ⊢  lift M 1 1 : lift N 1 1.
+
+axiom refl_conv: ∀A. conv A A.
+axiom  sym_conv: ∀A,B. conv A B → conv B A.
+axiom trans_conv: ∀A,B,C. conv A B → conv B C → conv A C.
+
+theorem prod_inv: ∀G,M,N. G ⊢ M : N → ∀A,B.M = Prod A B → 
+  ∃i,j,k. conv N (Sort k) ∧ G ⊢A : Sort i ∧ A::G ⊢B : Sort j. 
+#G #M #N #t (elim t);
+  [#i #j #Aij #A #b #H destruct
+  |#G1 #P #i #t #_ #A #b #H destruct
+  |#G1 #P #Q #R #i #t1 #t2 #H1 #_ #A #B #Hl
+   cases (prod_lift … Hl) #A1 * #B1 * * #eqP #eqA #eqB
+   cases (H1 … eqP) #i * #j * #k * * #c1 #t3 #t4
+   @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) <eqA <eqB %
+    [% [@(conv_lift … c1) |@(weak … t3 t2)]
+    |@(weak_in … t4 t2) 
+    ]
+  |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #B1 #H destruct
+   @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) % // % //
+  |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #B1 #H destruct
+  |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #B1 #H destruct
+  |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #B1 #eqA
+   cases (H1 … eqA) #i * #j * #k * * #c1 #t3 #t4
+   @(ex_intro … i) @(ex_intro … j) @(ex_intro … k) % //
+   % // @(trans_conv C B … c1) @sym_conv //
+  |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #B1 #eqA destruct
+  ]
+qed.
+
+theorem abs_inv: ∀G,M,N. G ⊢ M : N → ∀A,b.M = Lambda A b → 
+  ∃i,B. conv N (Prod A B) ∧ G ⊢Prod A B: Sort i ∧ A::G ⊢b : B. 
+#G #M #N #t (elim t);
+  [#i #j #Aij #A #b #H destruct
+  |#G1 #P #i #t #_ #A #b #H destruct
+  |#G1 #P #Q #R #i #t1 #t2 #H1 #_ #A #b #Hl
+   cases (lambda_lift … Hl) #A1 * #b1 * * #eqP #eqA #eqb
+   cases (H1 … eqP) #i * #B1 * * #c1 #t3 #t4
+   @(ex_intro … i) @(ex_intro … (lift B1 1 1)) <eqA <eqb %
+    [% [@(conv_lift … c1) |@(weak … t3 t2)]
+    |@(weak_in … t4 t2) 
+    ]
+  |#G1 #A #B #i #j #k #Rijk #t1 #t2 #_ #_ #A1 #b #H destruct
+  |#G1 #P #A #B #C #t1 #t2 #_ #_ #A1 #b #H destruct
+  |#G1 #P #A #B #i #t1 #t2 #_ #_ #A1 #b #H destruct
+    @(ex_intro … i) @(ex_intro … A) % // % //
+  |#G1 #A #B #C #i #cBC #t1 #t2 #H1 #H2 #A1 #b #eqA
+   cases (H1 … eqA) #i * #B1 * * #c1 #t3 #t4
+   @(ex_intro … i) @(ex_intro … B1) % //
+   % // @(trans_conv C B … c1) @sym_conv //
+  |#G1 #A #B #i #t1 #t2 #_ #_ #A1 #b #eqA destruct
+  ]
+qed.
+   
diff --git a/matita/matita/lib/lambda/subject.ma b/matita/matita/lib/lambda/subject.ma
new file mode 100644
index 000000000..c6b0eafdb
--- /dev/null
+++ b/matita/matita/lib/lambda/subject.ma
@@ -0,0 +1,263 @@
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department of the University of Bologna, Italy.                     
+    ||I||                                                                 
+    ||T||  
+    ||A||  This file is distributed under the terms of the 
+    \   /  GNU General Public License Version 2        
+     \ /      
+      V_______________________________________________________________ *)
+
+include "lambda/reduction.ma".
+include "lambda/inversion.ma". 
+
+(*
+inductive T : Type[0] ≝
+  | Sort: nat → T
+  | Rel: nat → T 
+  | App: T → T → T 
+  | Lambda: T → T → T (* type, body *)
+  | Prod: T → T → T (* type, body *)
+  | D: T →T
+. 
+
+inductive red : T →T → Prop ≝
+  | rbeta: ∀P,M,N. red (App (Lambda P M) N) (M[0 ≝ N])
+  | rdapp: ∀M,N. red (App (D M) N) (D (App M N))
+  | rdlam: ∀M,N. red (Lambda M (D N)) (D (Lambda M N))
+  | rappl: ∀M,M1,N. red M M1 → red (App M N) (App M1 N)
+  | rappr: ∀M,N,N1. red N N1 → red (App M N) (App M N1)
+  | rlaml: ∀M,M1,N. red M M1 → red (Lambda M N) (Lambda M1 N)
+  | rlamr: ∀M,N,N1. red N N1 → red(Lambda M N) (Lambda M N1)
+  | rprodl: ∀M,M1,N. red M M1 → red (Prod M N) (Prod M1 N)
+  | rprodr: ∀M,N,N1. red N N1 → red (Prod M N) (Prod M N1)
+  | d: ∀M,M1. red M M1 → red (D M) (D M1). *)
+  
+lemma lift_D: ∀M,N. lift M 0 1 = D N → 
+  ∃P. N = lift P 0 1 ∧ M = D P.   
+#M (cases M) normalize
+  [#i #N #H destruct
+  |#i #N #H destruct
+  |#A #B #N #H destruct
+  |#A #B #N #H destruct
+  |#A #B #N #H destruct
+  |#A #N #H destruct @(ex_intro … A) /2/
+  ]
+qed. 
+
+theorem type_of_type: ∀G,A,B. G ⊢ A : B → (∀i. B ≠ Sort i) →
+  ∃i. G ⊢ B : Sort i.
+#G #A #B #t (elim t)
+  [#i #j #Aij #j @False_ind /2/ 
+  |#G1 #A #i #t1 #_ #P @(ex_intro … i) @(weak … t1 t1)
+  |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 (cases (H1 ?) )
+    [#i #Bi @(ex_intro … i) @(weak … Bi t2)
+    |#i @(not_to_not … (H3 i)) //
+    ]
+  |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #H3 @False_ind /2/
+  |#G1 #A #B #C #D #t1 #t2 #H1 #H2 #H3 cases (H1 ?);
+    [#i #t3 cases (prod_inv … t3 … (refl …))
+     #s1 * #s2 * #s3 * * #Ci #H4 #H5 @(ex_intro … s2)
+     @(tj_subst_0 … t2 … H5)
+    |#i % #H destruct
+    ]  
+  |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #H3 /2/
+  |#G1 #A #B #C #i #ch #t1 #t2 #H1 #H2 #H3 /2/
+  |#G1 #A #B #i #t1 #t2 #Hind1 #Hind2 #H /2/
+  ]
+qed.
+
+lemma prod_sort : ∀G,M,P,Q. G ⊢ M :Prod P Q →
+ ∃i. P::G ⊢ Q : Sort i.
+#G #M #P #Q #t cases(type_of_type …t ?);
+  [#s #t2 cases(prod_inv … t2 …(refl …)) #s1 * #s2 * #s3 * * 
+   #_ #_ #H @(ex_intro … s2) //
+  | #i % #H destruct
+  ]
+qed.
+    
+axiom red_lift: ∀M,N. red (lift M 0 1) N → 
+  ∃P. N = lift P 0 1 ∧ red M P. 
+
+theorem tj_d : ∀G,M,N. G ⊢ D M : N → G ⊢ M : N.
+#G (cut (∀M,N. G ⊢ M : N → ∀P. M = D P → G ⊢ P : N)) [2: /2/] 
+#M #N #t (elim t)
+  [#i #j #Aij #P #H destruct 
+  |#G1 #A #i #t1 #_ #P #H destruct
+  |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #P #H3 
+   cases (lift_D … H3) #P * #eqP #eqA >eqP @(weak … i) /2/
+  |#G1 #A #B #i #j #k #h #t1 #t2 #_ #_ #P  #H destruct
+  |#G1 #A #B #C #D #t1 #t2 #_ #_ #P  #H destruct
+  |#G1 #A #B #C #D #t1 #t2 #_ #_ #P  #H destruct
+  |#G1 #A #B #C #i #ch #t1 #t2 #H #_ #P #H
+   @(conv… ch …t2) /2/
+  |#G1 #A #B #i #t1 #t2 #Hind1 #Hind2 #P #H destruct //
+  ]
+qed.
+
+definition red0 ≝ λM,N. M = N ∨ red M N.
+
+axiom conv_lift: ∀i,M,N. conv M N →
+  conv (lift M 0 i) (lift N 0 i).
+axiom red_to_conv : ∀M,N. red M N → conv M N.
+axiom refl_conv: ∀M. conv M M.
+axiom sym_conv: ∀M,N. conv M N → conv N M.
+axiom red0_to_conv : ∀M,N. red0 M N → conv M N.
+axiom conv_prod: ∀A,B,M,N. conv A B → conv M N → 
+  conv (Prod A M) (Prod B N). 
+axiom conv_subst_1: ∀M,P,Q. red P Q → conv (M[0≝Q]) (M[0≝P]).
+
+inductive redG : list T → list T → Prop ≝
+ | rnil : redG (nil T) (nil T)
+ | rstep : ∀A,B,G1,G2. red0 A B → redG G1 G2 → 
+     redG (A::G1) (B::G2).
+
+lemma redG_inv: ∀A,G,G1. redG (A::G) G1 → 
+  ∃B. ∃G2. red0 A B ∧ redG G G2 ∧ G1 = B::G2.
+#A #G #G1 #rg (inversion rg) 
+  [#H destruct
+  |#A1 #B1 #G2 #G3 #r1 #r2 #_ #H destruct
+   #H1 @(ex_intro … B1) @(ex_intro … G3) % // % //
+  ]
+qed.
+
+lemma redG_nil: ∀G. redG (nil T) G → G = nil T.
+#G #rg (inversion rg) // 
+#A #B #G1 #G2 #r1 #r2 #_ #H destruct
+qed.
+
+(*
+inductive redG : list T → list T → Prop ≝
+ |redT : ∀A,B,G1,G2. red A B → redG G1 G2 → 
+     redG (A::G1) (B::G2)
+ |redF : ∀A,G1,G2. redG G1 G2 → redG (A::G1) (A::G2).
+
+lemma redG_inv: ∀A,G,G1. redG (A::G) G1 → 
+  ∃B. ∃G2. red0 A B ∧ redG G G2 ∧ G1 = B::G2.
+#A #G #G1 #rg (inversion rg) 
+  [#H destruct
+  |#A1 #B1 #G2 #G3 #r1 #r2 #_ #H destruct
+   #H1 @(ex_intro … B1) @(ex_intro … G3) % // % //
+  ]
+qed. *)
+
+axiom conv_prod_split: ∀A,A1,B,B1. conv (Prod A B) (Prod A1 B1) →
+conv A A1 ∧ conv B B1.
+
+axiom red0_prod : ∀M,N,P. red0 (Prod M N) P → 
+  (∃Q. P = Prod Q N ∧ red0 M Q) ∨
+  (∃Q. P = Prod M Q ∧ red0 N Q).
+  
+axiom my_dummy: ∀G,M,N. G ⊢ M : N → G ⊢ D M : N.
+
+theorem subject_reduction: ∀G,M,N. TJ G M N → ∀M1. red0 M M1 → 
+∀G1. redG G G1 → TJ G1 M1 N.
+#G #M #N #d (elim d)
+  [#i #j #Aij #M1 * 
+    [#eqM1 <eqM1 #G1 #H >(redG_nil …H) /2/
+    |#H @False_ind /2/
+    ]
+  |#G1 #A #i #t1 #Hind #M1 * 
+    [#eqM1 <eqM1 #G2 #H cases (redG_inv … H)
+     #P * #G3 * * #r1 #r2 #eqG2 >eqG2
+     @(conv ?? (lift P O 1) ? i);
+      [@conv_lift @sym_conv @red0_to_conv //
+      |@(start … i) @Hind //
+      |@(weak … (Sort i) ? i); [@Hind /2/ | @Hind //]
+      ]
+    |#H @False_ind /2/
+    ]  
+  |#G1 #A #B #C #i #t1 #t2 #H1 #H2 #M1 
+   #H cases H;
+    [#eqM1 <eqM1 #G2 #rg (cases (redG_inv … rg)) 
+     #Q * #G3 * * #r2 #rg1 #eqG2 >eqG2 @(weak … i);
+      [@H1 /2/ | @H2 //] 
+    |#H (elim (red_lift … H)) #P * #eqM1 >eqM1 #redAP
+      #G2 #rg (cases (redG_inv … rg)) #Q * #G3 * * #r2 
+      #rg1 #eqG2 >eqG2 @(weak … i); 
+      [@H1 /2/ | @H2 //]
+    ]
+  |#G #A #B #i #j #k #Rjk #t1 #t2 #Hind1 #Hind2 #M1 #redP
+   (cases (red0_prod … redP))
+    [* #M2 * #eqM1 #redA >eqM1 #G1 #rg @(prod … Rjk);
+      [@Hind1 // | @Hind2 /2/]
+    |* #M2 * #eqM1 #redA >eqM1 #G1 #rg @(prod … Rjk); 
+      [@Hind1 /2/ | @Hind2 /3/] 
+    ]
+  |#G #A #B #C #P #t1 #t2 #Hind1 #Hind2 #M1 #red0a
+   (cases red0a)
+    [#eqM1 <eqM1 #G1 #rg @(app … B);
+      [@Hind1 /2/ | @Hind2 /2/ ]
+    |#reda (cases (red_app …reda))
+      [*
+        [* 
+          [* #M2 * #N1 * #eqA #eqM1 >eqM1 #G1 #rg
+           cut (G1 ⊢ A: Prod B C); [@Hind1 /2/] #H1
+           (cases (abs_inv … H1 … eqA)) #i * #N2 * * 
+           #cProd #t3 #t4 
+           (cut (conv B M2 ∧ conv C N2) ) [/2/] * #convB #convC
+           (cases (prod_inv … t3 … (refl …) )) #i * #j * #k * *
+           #cik #t5 #t6 (cut (G1 ⊢ P:B)) 
+            [@Hind2 /2/
+            |#Hcut cut (G1 ⊢ N1[0:=P] : N2 [0:=P]);
+              [@(tj_subst_0 … M2) // @(conv … convB Hcut t5)
+              |#Hcut1 cases (prod_sort … H1) #s #Csort
+               @(conv … s  … Hcut1); 
+                [@conv_subst /2/ | @(tj_subst_0 … Csort) //]
+              ]
+            ]
+          |* #M2 * #eqA #eqM1 >eqM1 #G1 #rg
+           cut (G1 ⊢ A:Prod B C); [@Hind1 /2/] #t3
+           cases (prod_sort …t3) #i #Csort @(dummy … i);
+            [ @(app  … B);
+              [@tj_d @Hind1 /2/|@Hind2 /2/]
+            | @(tj_subst_0 … B … (Sort i));
+              [@Hind2 /2/ 
+              |//
+              ]
+            ] 
+           (* @my_dummy @(app … B); [@tj_d @Hind1 /2/|@Hind2 /2/]
+           *)          
+          ]
+        |* #M2 * #eqM1 >eqM1 #H #G1 #rg @(app … B);
+          [@Hind1 /2/ | @Hind2 /2/] 
+        ]      
+      |* #M2 * #eqM1 >eqM1 #H #G1 #rg 
+       cut (G1 ⊢ A:Prod B C); [@Hind1 /2/] #t3
+       cases (prod_sort …t3) #i #Csort @(conv ?? C[O≝ M2] … i);
+        [@conv_subst_1 //
+        |@(app … B)  // @Hind2 /2/
+        |@(tj_subst_0 … Csort) @Hind2 /2/
+        ]
+      ]
+    ]
+  |#G #A #B #C #i #t1 #t2 #Hind1 #Hind2 #M2 #red0l #G1 #rg
+   cut (A::G1⊢C:B); [@Hind1 /3/] #t3
+   cut (G1 ⊢ Prod A B : Sort i); [@Hind2 /2/] #t4
+   cases red0l;
+    [#eqM2 <eqM2 @(abs … t3 t4)
+    |#redl (cases (red_lambda … redl))  
+      [*
+        [* #M3 * #eqM2 #redA >eqM2 
+         @(conv ?? (Prod M3 B) … t4);
+          [@conv_prod /2/
+          |@(abs … i); [@Hind1 /3/ |@Hind2 /3/]
+          ]
+        |* #M3 * #eqM3 #redC >eqM3
+         @(abs … t4) @Hind1 /3/
+        ]
+      |* #Q * #eqC #eqM2 >eqM2 @(dummy … t4)
+       @(abs … t4) @tj_d @Hind1 /3/
+      ]
+    ]
+  |#G #A #B #C #i #convBC #t1 #t2 #Hind1 #Hind2 #M1 #redA
+   #G1 #rg @(conv … i … convBC); [@Hind1 // |@Hind2 /2/]
+  |#G #A #B #i #t1 #t2 #Hind1 #Hind2 #M1 #red0d #G1 #rg
+   cases red0d; 
+    [#eqM1 <eqM1 @(dummy … i); [@Hind1 /2/ |@Hind2 /2/] 
+    |#redd (cases (red_d … redd)) #Q * #eqM1 #redA >eqM1
+     @(dummy … i);[@Hind1 /2/ |@Hind2 /2/]
+  ]
+qed.
+
-- 
2.39.2