contribution about \lambda-\delta

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / base_types.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/base_types.v b/helm/coq-contribs/LAMBDA-TYPES/base_types.v
new file mode 100644 (file)
index 0000000..0b1c870
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/base_types.v
@@ -0,0 +1,159 @@
+(* This file was generated by coqgen *)
+
+Require base_tactics.
+Require base_hints.
+
+(*#* #stop file *)
+
+(* extensions for ex2 *)
+
+Syntactic Definition ex2_intro := ex_intro2.
+
+Theorem ex2_sym: (A:Set; P,Q:A->Prop)
+                 (EX x | (P x) & (Q x)) -> (EX x | (Q x) & (P x)).
+                 Intros; XElim H; XEAuto.
+                 Qed.
+
+Hints Resolve ex2_sym : ltlc.
+
+(* or3 *)
+
+Inductive or3 [P0,P1,P2:Prop] : Prop :=
+   | or3_intro0 : P0 -> (or3 P0 P1 P2)
+   | or3_intro1 : P1 -> (or3 P0 P1 P2)
+   | or3_intro2 : P2 -> (or3 P0 P1 P2).
+
+Hint or3 : ltlc := Constructors or3.
+
+Grammar constr constr10 :=
+   | or3
+      [ "OR" constr($c0) "|" constr($c1) "|" constr($c2) ] ->
+      [ (or3 $c0 $c1 $c2) ].
+
+(* or4 *)
+
+Inductive or4 [P0,P1,P2,P3:Prop] : Prop :=
+   | or4_intro0 : P0 -> (or4 P0 P1 P2 P3)
+   | or4_intro1 : P1 -> (or4 P0 P1 P2 P3)
+   | or4_intro2 : P2 -> (or4 P0 P1 P2 P3)
+   | or4_intro3 : P3 -> (or4 P0 P1 P2 P3).
+
+Hint or4 : ltlc := Constructors or4.
+
+Grammar constr constr10 :=
+   | or4
+      [ "OR" constr($c0) "|" constr($c1) "|" constr($c2) "|" constr($c3) ] ->
+      [ (or4 $c0 $c1 $c2 $c3) ].
+
+(* ex2_2 *)
+
+Inductive ex2_2 [A0,A1:Set; P0,P1:A0->A1->Prop] : Prop := 
+   ex2_2_intro : (x0:A0; x1:A1)(P0 x0 x1)->(P1 x0 x1)->(ex2_2 A0 A1 P0 P1).
+
+Hint ex2_2 : ltlc := Constructors ex2_2.
+
+Syntactic Definition Ex2_2 := ex2_2 | 1.
+
+Grammar constr constr10 :=
+   | ex2_2implicit
+      [ "EX" ident($v0) ident($v1) "|" constr($c0) "&" constr($c1) ] ->
+      [ (ex2_2 ? ? [$v0;$v1]$c0 [$v0;$v1]$c1) ].
+
+(* ex3_2 *)
+
+Inductive ex3_2 [A0,A1:Set; P0,P1,P2:A0->A1->Prop] : Prop := 
+   ex3_2_intro : (x0:A0; x1:A1)(P0 x0 x1)->(P1 x0 x1)->(P2 x0 x1)->(ex3_2 A0 A1 P0 P1 P2).
+
+Hint ex3_2 : ltlc := Constructors ex3_2.
+
+Syntactic Definition Ex3_2 := ex3_2 | 1.
+
+Grammar constr constr10 :=
+   | ex3_2implicit
+      [ "EX" ident($v0) ident($v1) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
+      [ (ex3_2 ? ? [$v0;$v1]$c0 [$v0;$v1]$c1 [$v0;$v1]$c2) ].
+
+(* ex3_3 *)
+
+Inductive ex3_3 [A0,A1,A2:Set; P0,P1,P2:A0->A1->A2->Prop] : Prop := 
+   ex3_3_intro : (x0:A0; x1:A1; x2:A2)(P0 x0 x1 x2)->(P1 x0 x1 x2)->(P2 x0 x1 x2)->(ex3_3 A0 A1 A2 P0 P1 P2).
+
+Hint ex3_3 : ltlc := Constructors ex3_3.
+
+Syntactic Definition Ex3_3 := ex3_3 | 1.
+
+Grammar constr constr10 :=
+   | ex3_3implicit
+      [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
+      [ (ex3_3 ? ? ? [$v0;$v1;$v2]$c0 [$v0;$v1;$v2]$c1 [$v0;$v1;$v2]$c2) ].
+
+(* ex4_3 *)
+
+Inductive ex4_3 [A0,A1,A2:Set; P0,P1,P2,P3:A0->A1->A2->Prop] : Prop := 
+   ex4_3_intro : (x0:A0; x1:A1; x2:A2)(P0 x0 x1 x2)->(P1 x0 x1 x2)->(P2 x0 x1 x2)->(P3 x0 x1 x2)->(ex4_3 A0 A1 A2 P0 P1 P2 P3).
+
+Hint ex4_3 : ltlc := Constructors ex4_3.
+
+Syntactic Definition Ex4_3 := ex4_3 | 1.
+
+Grammar constr constr10 :=
+   | ex4_3implicit
+      [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
+      [ (ex4_3 ? ? ? [$v0;$v1;$v2]$c0 [$v0;$v1;$v2]$c1 [$v0;$v1;$v2]$c2 [$v0;$v1;$v2]$c3) ].
+
+(* ex3_4 *)
+
+Inductive ex3_4 [A0,A1,A2,A3:Set; P0,P1,P2:A0->A1->A2->A3->Prop] : Prop := 
+   ex3_4_intro : (x0:A0; x1:A1; x2:A2; x3:A3)(P0 x0 x1 x2 x3)->(P1 x0 x1 x2 x3)->(P2 x0 x1 x2 x3)->(ex3_4 A0 A1 A2 A3 P0 P1 P2).
+
+Hint ex3_4 : ltlc := Constructors ex3_4.
+
+Syntactic Definition Ex3_4 := ex3_4 | 1.
+
+Grammar constr constr10 :=
+   | ex3_4implicit
+      [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
+      [ (ex3_4 ? ? ? ? [$v0;$v1;$v2;$v3]$c0 [$v0;$v1;$v2;$v3]$c1 [$v0;$v1;$v2;$v3]$c2) ].
+
+(* ex4_4 *)
+
+Inductive ex4_4 [A0,A1,A2,A3:Set; P0,P1,P2,P3:A0->A1->A2->A3->Prop] : Prop := 
+   ex4_4_intro : (x0:A0; x1:A1; x2:A2; x3:A3)(P0 x0 x1 x2 x3)->(P1 x0 x1 x2 x3)->(P2 x0 x1 x2 x3)->(P3 x0 x1 x2 x3)->(ex4_4 A0 A1 A2 A3 P0 P1 P2 P3).
+
+Hint ex4_4 : ltlc := Constructors ex4_4.
+
+Syntactic Definition Ex4_4 := ex4_4 | 1.
+
+Grammar constr constr10 :=
+   | ex4_4implicit
+      [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
+      [ (ex4_4 ? ? ? ? [$v0;$v1;$v2;$v3]$c0 [$v0;$v1;$v2;$v3]$c1 [$v0;$v1;$v2;$v3]$c2 [$v0;$v1;$v2;$v3]$c3) ].
+
+(* ex4_5 *)
+
+Inductive ex4_5 [A0,A1,A2,A3,A4:Set; P0,P1,P2,P3:A0->A1->A2->A3->A4->Prop] : Prop := 
+   ex4_5_intro : (x0:A0; x1:A1; x2:A2; x3:A3; x4:A4)(P0 x0 x1 x2 x3 x4)->(P1 x0 x1 x2 x3 x4)->(P2 x0 x1 x2 x3 x4)->(P3 x0 x1 x2 x3 x4)->(ex4_5 A0 A1 A2 A3 A4 P0 P1 P2 P3).
+
+Hint ex4_5 : ltlc := Constructors ex4_5.
+
+Syntactic Definition Ex4_5 := ex4_5 | 1.
+
+Grammar constr constr10 :=
+   | ex4_5implicit
+      [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
+      [ (ex4_5 ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4]$c0 [$v0;$v1;$v2;$v3;$v4]$c1 [$v0;$v1;$v2;$v3;$v4]$c2 [$v0;$v1;$v2;$v3;$v4]$c3) ].
+
+(* ex6_6 *)
+
+Inductive ex6_6 [A0,A1,A2,A3,A4,A5:Set; P0,P1,P2,P3,P4,P5:A0->A1->A2->A3->A4->A5->Prop] : Prop := 
+   ex6_6_intro : (x0:A0; x1:A1; x2:A2; x3:A3; x4:A4; x5:A5)(P0 x0 x1 x2 x3 x4 x5)->(P1 x0 x1 x2 x3 x4 x5)->(P2 x0 x1 x2 x3 x4 x5)->(P3 x0 x1 x2 x3 x4 x5)->(P4 x0 x1 x2 x3 x4 x5)->(P5 x0 x1 x2 x3 x4 x5)->(ex6_6 A0 A1 A2 A3 A4 A5 P0 P1 P2 P3 P4 P5).
+
+Hint ex6_6 : ltlc := Constructors ex6_6.
+
+Syntactic Definition Ex6_6 := ex6_6 | 1.
+
+Grammar constr constr10 :=
+   | ex6_6implicit
+      [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) ident($v5) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) "&" constr($c5) ] ->
+      [ (ex6_6 ? ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4;$v5]$c0 [$v0;$v1;$v2;$v3;$v4;$v5]$c1 [$v0;$v1;$v2;$v3;$v4;$v5]$c2 [$v0;$v1;$v2;$v3;$v4;$v5]$c3 [$v0;$v1;$v2;$v3;$v4;$v5]$c4 [$v0;$v1;$v2;$v3;$v4;$v5]$c5) ].
+