helm/coq-contribs/LAMBDA-TYPES/base_types.v

   1 (* This file was generated by coqgen *)
   2
   3 Require base_tactics.
   4 Require base_hints.
   5
   6 (*#* #stop file *)
   7
   8 (* extensions for ex2 *)
   9
  10 Syntactic Definition ex2_intro := ex_intro2.
  11
  12 Theorem ex2_sym: (A:Set; P,Q:A->Prop)
  13                  (EX x | (P x) & (Q x)) -> (EX x | (Q x) & (P x)).
  14                  Intros; XElim H; XEAuto.
  15                  Qed.
  16
  17 Hints Resolve ex2_sym : ltlc.
  18
  19 (* or3 *)
  20
  21 Inductive or3 [P0,P1,P2:Prop] : Prop :=
  22    | or3_intro0 : P0 -> (or3 P0 P1 P2)
  23    | or3_intro1 : P1 -> (or3 P0 P1 P2)
  24    | or3_intro2 : P2 -> (or3 P0 P1 P2).
  25
  26 Hint or3 : ltlc := Constructors or3.
  27
  28 Grammar constr constr10 :=
  29    | or3
  30       [ "OR" constr($c0) "|" constr($c1) "|" constr($c2) ] ->
  31       [ (or3 $c0 $c1 $c2) ].
  32
  33 (* or4 *)
  34
  35 Inductive or4 [P0,P1,P2,P3:Prop] : Prop :=
  36    | or4_intro0 : P0 -> (or4 P0 P1 P2 P3)
  37    | or4_intro1 : P1 -> (or4 P0 P1 P2 P3)
  38    | or4_intro2 : P2 -> (or4 P0 P1 P2 P3)
  39    | or4_intro3 : P3 -> (or4 P0 P1 P2 P3).
  40
  41 Hint or4 : ltlc := Constructors or4.
  42
  43 Grammar constr constr10 :=
  44    | or4
  45       [ "OR" constr($c0) "|" constr($c1) "|" constr($c2) "|" constr($c3) ] ->
  46       [ (or4 $c0 $c1 $c2 $c3) ].
  47
  48 (* ex2_2 *)
  49
  50 Inductive ex2_2 [A0,A1:Set; P0,P1:A0->A1->Prop] : Prop :=
  51    ex2_2_intro : (x0:A0; x1:A1)(P0 x0 x1)->(P1 x0 x1)->(ex2_2 A0 A1 P0 P1).
  52
  53 Hint ex2_2 : ltlc := Constructors ex2_2.
  54
  55 Syntactic Definition Ex2_2 := ex2_2 | 1.
  56
  57 Grammar constr constr10 :=
  58    | ex2_2implicit
  59       [ "EX" ident($v0) ident($v1) "|" constr($c0) "&" constr($c1) ] ->
  60       [ (ex2_2 ? ? [$v0;$v1]$c0 [$v0;$v1]$c1) ].
  61
  62 (* ex3_2 *)
  63
  64 Inductive ex3_2 [A0,A1:Set; P0,P1,P2:A0->A1->Prop] : Prop :=
  65    ex3_2_intro : (x0:A0; x1:A1)(P0 x0 x1)->(P1 x0 x1)->(P2 x0 x1)->(ex3_2 A0 A1 P0 P1 P2).
  66
  67 Hint ex3_2 : ltlc := Constructors ex3_2.
  68
  69 Syntactic Definition Ex3_2 := ex3_2 | 1.
  70
  71 Grammar constr constr10 :=
  72    | ex3_2implicit
  73       [ "EX" ident($v0) ident($v1) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
  74       [ (ex3_2 ? ? [$v0;$v1]$c0 [$v0;$v1]$c1 [$v0;$v1]$c2) ].
  75
  76 (* ex_3 *)
  77
  78 Inductive ex_3 [A0,A1,A2:Set; P0:A0->A1->A2->Prop] : Prop :=
  79    ex_3_intro : (x0:A0; x1:A1; x2:A2)(P0 x0 x1 x2)->(ex_3 A0 A1 A2 P0).
  80
  81 Hint ex_3 : ltlc := Constructors ex_3.
  82
  83 Syntactic Definition Ex_3 := ex_3 | 1.
  84
  85 Grammar constr constr10 :=
  86    | ex_3implicit
  87       [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) ] ->
  88       [ (ex_3 ? ? ? [$v0;$v1;$v2]$c0) ].
  89
  90 (* ex3_3 *)
  91
  92 Inductive ex3_3 [A0,A1,A2:Set; P0,P1,P2:A0->A1->A2->Prop] : Prop :=
  93    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).
  94
  95 Hint ex3_3 : ltlc := Constructors ex3_3.
  96
  97 Syntactic Definition Ex3_3 := ex3_3 | 1.
  98
  99 Grammar constr constr10 :=
 100    | ex3_3implicit
 101       [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
 102       [ (ex3_3 ? ? ? [$v0;$v1;$v2]$c0 [$v0;$v1;$v2]$c1 [$v0;$v1;$v2]$c2) ].
 103
 104 (* ex4_3 *)
 105
 106 Inductive ex4_3 [A0,A1,A2:Set; P0,P1,P2,P3:A0->A1->A2->Prop] : Prop :=
 107    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).
 108
 109 Hint ex4_3 : ltlc := Constructors ex4_3.
 110
 111 Syntactic Definition Ex4_3 := ex4_3 | 1.
 112
 113 Grammar constr constr10 :=
 114    | ex4_3implicit
 115       [ "EX" ident($v0) ident($v1) ident($v2) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
 116       [ (ex4_3 ? ? ? [$v0;$v1;$v2]$c0 [$v0;$v1;$v2]$c1 [$v0;$v1;$v2]$c2 [$v0;$v1;$v2]$c3) ].
 117
 118 (* ex3_4 *)
 119
 120 Inductive ex3_4 [A0,A1,A2,A3:Set; P0,P1,P2:A0->A1->A2->A3->Prop] : Prop :=
 121    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).
 122
 123 Hint ex3_4 : ltlc := Constructors ex3_4.
 124
 125 Syntactic Definition Ex3_4 := ex3_4 | 1.
 126
 127 Grammar constr constr10 :=
 128    | ex3_4implicit
 129       [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) "|" constr($c0) "&" constr($c1) "&" constr($c2) ] ->
 130       [ (ex3_4 ? ? ? ? [$v0;$v1;$v2;$v3]$c0 [$v0;$v1;$v2;$v3]$c1 [$v0;$v1;$v2;$v3]$c2) ].
 131
 132 (* ex4_4 *)
 133
 134 Inductive ex4_4 [A0,A1,A2,A3:Set; P0,P1,P2,P3:A0->A1->A2->A3->Prop] : Prop :=
 135    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).
 136
 137 Hint ex4_4 : ltlc := Constructors ex4_4.
 138
 139 Syntactic Definition Ex4_4 := ex4_4 | 1.
 140
 141 Grammar constr constr10 :=
 142    | ex4_4implicit
 143       [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
 144       [ (ex4_4 ? ? ? ? [$v0;$v1;$v2;$v3]$c0 [$v0;$v1;$v2;$v3]$c1 [$v0;$v1;$v2;$v3]$c2 [$v0;$v1;$v2;$v3]$c3) ].
 145
 146 (* ex4_5 *)
 147
 148 Inductive ex4_5 [A0,A1,A2,A3,A4:Set; P0,P1,P2,P3:A0->A1->A2->A3->A4->Prop] : Prop :=
 149    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).
 150
 151 Hint ex4_5 : ltlc := Constructors ex4_5.
 152
 153 Syntactic Definition Ex4_5 := ex4_5 | 1.
 154
 155 Grammar constr constr10 :=
 156    | ex4_5implicit
 157       [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) ] ->
 158       [ (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) ].
 159
 160 (* ex5_5 *)
 161
 162 Inductive ex5_5 [A0,A1,A2,A3,A4:Set; P0,P1,P2,P3,P4:A0->A1->A2->A3->A4->Prop] : Prop :=
 163    ex5_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)->(P4 x0 x1 x2 x3 x4)->(ex5_5 A0 A1 A2 A3 A4 P0 P1 P2 P3 P4).
 164
 165 Hint ex5_5 : ltlc := Constructors ex5_5.
 166
 167 Syntactic Definition Ex5_5 := ex5_5 | 1.
 168
 169 Grammar constr constr10 :=
 170    | ex5_5implicit
 171       [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) ] ->
 172       [ (ex5_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 [$v0;$v1;$v2;$v3;$v4]$c4) ].
 173
 174 (* ex6_6 *)
 175
 176 Inductive ex6_6 [A0,A1,A2,A3,A4,A5:Set; P0,P1,P2,P3,P4,P5:A0->A1->A2->A3->A4->A5->Prop] : Prop :=
 177    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).
 178
 179 Hint ex6_6 : ltlc := Constructors ex6_6.
 180
 181 Syntactic Definition Ex6_6 := ex6_6 | 1.
 182
 183 Grammar constr constr10 :=
 184    | ex6_6implicit
 185       [ "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) ] ->
 186       [ (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) ].
 187
 188 (* ex6_7 *)
 189
 190 Inductive ex6_7 [A0,A1,A2,A3,A4,A5,A6:Set; P0,P1,P2,P3,P4,P5:A0->A1->A2->A3->A4->A5->A6->Prop] : Prop :=
 191    ex6_7_intro : (x0:A0; x1:A1; x2:A2; x3:A3; x4:A4; x5:A5; x6:A6)(P0 x0 x1 x2 x3 x4 x5 x6)->(P1 x0 x1 x2 x3 x4 x5 x6)->(P2 x0 x1 x2 x3 x4 x5 x6)->(P3 x0 x1 x2 x3 x4 x5 x6)->(P4 x0 x1 x2 x3 x4 x5 x6)->(P5 x0 x1 x2 x3 x4 x5 x6)->(ex6_7 A0 A1 A2 A3 A4 A5 A6 P0 P1 P2 P3 P4 P5).
 192
 193 Hint ex6_7 : ltlc := Constructors ex6_7.
 194
 195 Syntactic Definition Ex6_7 := ex6_7 | 1.
 196
 197 Grammar constr constr10 :=
 198    | ex6_7implicit
 199       [ "EX" ident($v0) ident($v1) ident($v2) ident($v3) ident($v4) ident($v5) ident($v6) "|" constr($c0) "&" constr($c1) "&" constr($c2) "&" constr($c3) "&" constr($c4) "&" constr($c5) ] ->
 200       [ (ex6_7 ? ? ? ? ? ? ? [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c0 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c1 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c2 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c3 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c4 [$v0;$v1;$v2;$v3;$v4;$v5;$v6]$c5) ].
 201
 202 (* extended Decompose tactic *)
 203
 204 Tactic Definition XDecompose H :=
 205    Decompose [and or ex ex2 or3 or4 ex2_2 ex3_2 ex_3 ex3_3 ex4_3 ex3_4 ex4_4 ex4_5 ex5_5 ex6_6 ex6_7] H; Clear H.
 206