X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_defs.v;fp=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_defs.v;h=3c7a96bbe3b2a081fec712691f7984f2001cd4e4;hb=1b21075e987872a2e3103203b4e67c939e4a9f6a;hp=0000000000000000000000000000000000000000;hpb=ea6b99ed26a954a578e3c88909479dcf9cab7345;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
new file mode 100644
index 000000000..3c7a96bbe
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
@@ -0,0 +1,91 @@
+(*#* #stop file *)
+
+Require Export subst0_defs.
+
+      Inductive pr0 : T -> T -> Prop :=
+(* structural rules *)
+         | pr0_refl  : (t:?) (pr0 t t)
+         | pr0_thin  : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+                       (k:?) (pr0 (TTail k u1 t1) (TTail k u2 t2))
+(* axiom rules *)
+         | pr0_beta  : (k,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
+                       (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) k t1))
+                            (TTail (Bind Abbr) v2 t2))
+         | pr0_gamma : (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
+                       (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+                       (pr0 (TTail (Flat Appl) v1 (TTail (Bind b) u1 t1))
+                            (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)))
+         | pr0_delta : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
+                       (w:?) (subst0 (0) u2 t2 w) ->
+                       (pr0 (TTail (Bind Abbr) u1 t1) (TTail (Bind Abbr) u2 w))
+         | pr0_zeta  : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
+                       (u:?) (pr0 (TTail (Bind b) u (lift (1) (0) t1)) t2)
+         | pr0_eps   : (t1,t2:?) (pr0 t1 t2) ->
+                       (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
+
+      Hint pr0 : ltlc := Constructors pr0.
+
+   Section pr0_gen. (********************************************************)
+
+      Theorem pr0_gen_sort : (x:?; n:?) (pr0 (TSort n) x) -> x = (TSort n).
+      Intros; Inversion H; XAuto.
+      Qed.
+
+      Theorem pr0_gen_bref : (x:?; n:?) (pr0 (TBRef n) x) -> x = (TBRef n).
+      Intros; Inversion H; XAuto.
+      Qed.
+
+      Theorem pr0_gen_abst : (u1,t1,x:?) (pr0 (TTail (Bind Abst) u1 t1) x) ->
+                             (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
+                                         (pr0 u1 u2) & (pr0 t1 t2)
+                             ).
+
+      Intros; Inversion H; Clear H.
+(* case 1 : pr0_refl *)
+      XEAuto.
+(* case 2 : pr0_cont *)
+      XEAuto.
+(* case 3 : pr0_zeta *)
+      XElim H4; XAuto.
+      Qed.
+
+      Theorem pr0_gen_appl : (u1,t1,x:?) (pr0 (TTail (Flat Appl) u1 t1) x) -> (OR
+                             (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
+                                         (pr0 u1 u2) & (pr0 t1 t2)
+                             ) |
+                             (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
+                                               x = (TTail (Bind Abbr) u2 t2) &
+                                               (pr0 u1 u2) & (pr0 z1 t2)
+                             ) |
+                             (EX b y1 z1 u2 v2 t2 |
+                                ~b=Abst &
+                                t1 = (TTail (Bind b) y1 z1) &
+                                x = (TTail (Bind b) v2 (TTail (Flat Appl) (lift (1) (0) u2) t2)) &
+                                (pr0 u1 u2) & (pr0 y1 v2) & (pr0 z1 t2))
+                             ).
+      Intros; Inversion H; XEAuto.
+      Qed.
+
+      Theorem pr0_gen_cast : (u1,t1,x:?) (pr0 (TTail (Flat Cast) u1 t1) x) ->
+                             (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
+                                         (pr0 u1 u2) & (pr0 t1 t2)
+                             ) \/
+                            (pr0 t1 x).
+      Intros; Inversion H; XEAuto.
+      Qed.
+
+   End pr0_gen.
+
+      Hints Resolve pr0_gen_sort pr0_gen_bref : ltlc.
+
+      Tactic Definition Pr0GenBase :=
+         Match Context With
+            | [ H: (pr0 (TTail (Bind Abst) ?1 ?2) ?3) |- ? ] ->
+               LApply (pr0_gen_abst ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
+               XElim H; Intros
+            | [ H: (pr0 (TTail (Flat Appl) ?1 ?2) ?3) |- ? ] ->
+               LApply (pr0_gen_appl ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
+               XElim H; Intros H; XElim H; Intros
+            | [ H: (pr0 (TTail (Flat Cast) ?1 ?2) ?3) |- ? ] ->
+               LApply (pr0_gen_cast ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
+               XElim H; [ Intros H; XElim H; Intros | Intros ].