1
(****************************************************************************)
2
(* Pattern-matching when non inductive terms occur *)
4
(* Dependent form of annotation *)
5
Type match 0 as n, eq return nat with
9
Type match 0, eq, 0 return nat with
13
Type match 0, eq, 0 return _ with
18
(* Non dependent form of annotation *)
19
Type match 0, eq return nat with
24
(* Combining dependencies and non inductive arguments *)
26
(fun (A : Set) (a : A) (H : 0 = 0) =>
27
match H in (_ = x), a return (H = H) with
28
| _, _ => refl_equal H
31
(* Interaction with coercions *)
32
Parameter bool2nat : bool -> nat.
33
Coercion bool2nat : bool >-> nat.
34
Check (fun x => match x with
39
(****************************************************************************)
40
(* All remaining examples come from Cristina Cornes' V6 TESTS/MultCases.v *)
42
Inductive IFExpr : Set :=
46
| IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr.
48
Inductive List (A : Set) : Set :=
50
| Cons : A -> List A -> List A.
52
Inductive listn : nat -> Set :=
54
| consn : forall n : nat, nat -> listn n -> listn (S n).
56
Inductive Listn (A : Set) : nat -> Set :=
58
| Consn : forall n : nat, nat -> Listn A n -> Listn A (S n).
60
Inductive Le : nat -> nat -> Set :=
61
| LeO : forall n : nat, Le 0 n
62
| LeS : forall n m : nat, Le n m -> Le (S n) (S m).
64
Inductive LE (n : nat) : nat -> Set :=
66
| LE_S : forall m : nat, LE n m -> LE n (S m).
72
Inductive PropForm : Set :=
73
| Fvar : nat -> PropForm
74
| Or : PropForm -> PropForm -> PropForm.
77
Definition Assign := nat -> bool.
78
Parameter Prop_sem : Assign -> PropForm -> bool.
81
(fun (A : Assign) (F : PropForm) =>
82
match F return bool with
84
| Or F G => Prop_sem A F || Prop_sem A G
88
(fun (A : Assign) (H : PropForm) =>
89
match H return bool with
91
| Or F G => Prop_sem A F || Prop_sem A G
97
Type (fun x : nat => match x return nat with
104
Inductive list : Set :=
106
| cons : A -> list -> list.
107
Parameter inf : A -> A -> Prop.
110
Definition list_Lowert2 (a : A) (l : list) :=
111
match l return Prop with
113
| cons b l => inf a b
116
Definition titi (a : A) (l : list) :=
117
match l return list with
125
(* To test translation *)
126
(* ------------------- *)
129
Type match 0 return nat with
134
Type match 0 return nat with
147
Type (fun x : nat => match x return nat with
152
Type (fun x : nat => match x with
157
Type match 0 return nat with
162
Type match 0 return nat with
170
Type match 0 return nat with
175
Type (fun x : nat => match x return nat with
180
Type (fun x : nat => match x with
186
Type match 0 return nat with
192
Type match 0 return (nat * nat) with
203
match 0 return (nat -> nat) with
204
| O => fun n : nat => 0
205
| S x => fun n : nat => 0
209
| O => fun n : nat => 0
210
| S x => fun n : nat => 0
215
match 0 return (nat -> nat) with
216
| O => fun n : nat => 0
217
| S x => fun n : nat => x + n
221
| O => fun n : nat => 0
222
| S x => fun n : nat => x + n
226
Type match 0 return nat with
231
Type match 0 return nat with
246
Type match 0 return nat with
251
Type match 0, 1 return nat with
259
Type match 0, 1 return nat with
270
Type match 0, 1 return nat with
286
match 0, 1 return nat with
294
match 0, 1 return nat with
296
| S x as b, S y => b + x + y
304
| S x as b, S y => b + x + y
311
match l return (List nat) with
316
Type (fun l : List nat => match l with
321
Type match Nil nat return nat with
325
Type match Nil nat with
330
Type match Nil nat return (List nat) with
335
Type match Nil nat with
341
match Nil nat return (List nat) with
346
Type match Nil nat with
353
match 0 return nat with
355
| S x => match Nil nat return nat with
364
| S x => match Nil nat with
374
| S x => match Nil nat with
382
match 0, Nil nat return nat with
385
| S x, Cons a l => x + a
391
(fun (n : nat) (l : listn n) =>
392
match l return nat with
397
Type (fun (n : nat) (l : listn n) => match l with
403
Type match niln return nat with
413
Type match niln return nat with
424
match niln in (listn n) return nat with
425
| consn m _ niln => m
432
(fun (n x : nat) (l : listn n) =>
433
match x, l return nat with
438
Type match 0, niln return nat with
444
Type match niln, 0 return nat with
449
Type match niln, 0 with
454
Type match niln, niln return nat with
459
Type match niln, niln with
465
match niln, niln, niln return nat with
466
| niln, niln, niln => 0
471
Type match niln, niln, niln with
472
| niln, niln, niln => 0
478
Type match niln return nat with
490
match niln, niln return nat with
492
| niln, consn n a l => n
493
| consn n a l, x => a
498
match niln, niln with
500
| niln, consn n a l => n
501
| consn n a l, x => a
506
(fun (n : nat) (l : listn n) =>
507
match l return nat with
513
(fun (c : nat) (s : bool) =>
514
match c, s return nat with
520
(fun (c : nat) (s : bool) =>
521
match c, s return nat with
527
(* Rows of pattern variables: some tricky cases *)
528
Axioms (P : nat -> Prop) (f : forall n : nat, P n).
532
match true, i as n return (P n) with
539
match i as n, true return (P n) with
544
(* Nested Cases: the SYNTH of the Cases on n used to make Multcase believe
545
* it has to synthtize the predicate on O (which he can't)
548
match 0 as n return match n with
556
Type (fun (n : nat) (l : listn n) => match l with
562
(fun (n : nat) (l : listn n) =>
563
match l return nat with
565
| consn n a niln => 0
566
| consn n a (consn m b l) => n + m
571
(fun (n : nat) (l : listn n) =>
574
| consn n a niln => 0
575
| consn n a (consn m b l) => n + m
581
(fun (n : nat) (l : listn n) =>
582
match l return nat with
584
| consn n a niln => 0
585
| consn n a (consn m b l) => n + m
589
(fun (n : nat) (l : listn n) =>
592
| consn n a niln => 0
593
| consn n a (consn m b l) => n + m
598
(fun (A : Set) (n : nat) (l : Listn A n) =>
599
match l return nat with
601
| Consn n a Niln => 0
602
| Consn n a (Consn m b l) => n + m
606
(fun (A : Set) (n : nat) (l : Listn A n) =>
609
| Consn n a Niln => 0
610
| Consn n a (Consn m b l) => n + m
614
Type [A:Set][n:nat][l:(Listn A n)]
615
<[_:nat](Listn A O)>Cases l of
617
| (Consn n a (Niln as b))=> (Niln A)
618
| (Consn n a (Consn m b l)) => (Niln A)
621
Type [A:Set][n:nat][l:(Listn A n)]
624
| (Consn n a (Niln as b))=> (Niln A)
625
| (Consn n a (Consn m b l)) => (Niln A)
628
(******** This example rises an error unconstrained_variables!
629
Type [A:Set][n:nat][l:(Listn A n)]
631
(Niln as b) => (Consn A O O b)
632
| ((Consn n a Niln) as L) => L
633
| (Consn n a _) => (Consn A O O (Niln A))
637
(* To test tratement of as-patterns in depth *)
639
(fun (A : Set) (l : List A) =>
642
| Cons a Nil as L => L
643
| Cons a (Cons b m) as L => L
648
(fun (n : nat) (l : listn n) =>
649
match l return (listn n) with
654
(fun (n : nat) (l : listn n) =>
662
(fun (n : nat) (l : listn n) =>
663
match l return (listn n) with
670
(fun (n : nat) (l : listn n) => match l with
676
(fun (n : nat) (l : listn n) =>
677
match l return (listn n) with
684
(fun (A : Set) (n : nat) (l : Listn A n) =>
691
(fun (A : Set) (n : nat) (l : Listn A n) =>
692
match l return (Listn A n) with
694
| Consn n a Niln => l
695
| Consn n a (Consn m b c) => l
699
(fun (A : Set) (n : nat) (l : Listn A n) =>
702
| Consn n a Niln => l
703
| Consn n a (Consn m b c) => l
707
(fun (A : Set) (n : nat) (l : Listn A n) =>
708
match l return (Listn A n) with
710
| Consn n a (Niln as b) => l
711
| Consn n a (Consn m b _) => l
715
(fun (A : Set) (n : nat) (l : Listn A n) =>
718
| Consn n a (Niln as b) => l
719
| Consn n a (Consn m b _) => l
724
match niln return nat with
726
| consn n a niln => 0
727
| consn n a (consn m b l) => n + m
734
| consn n a niln => 0
735
| consn n a (consn m b l) => n + m
738
Type match LeO 0 return nat with
744
Type match LeO 0 with
750
(fun (n : nat) (l : Listn nat n) =>
751
match l return nat with
758
(fun (n : nat) (l : Listn nat n) =>
765
Type match Niln nat with
770
Type match LE_n 0 return nat with
776
Type match LE_n 0 with
783
Type match LE_n 0 with
791
match niln return nat with
793
| consn n a niln => n
794
| consn n a (consn m b l) => n + m
800
| consn n a niln => n
801
| consn n a (consn m b l) => n + m
806
match Niln nat return nat with
808
| Consn n a Niln => n
809
| Consn n a (Consn m b l) => n + m
815
| Consn n a Niln => n
816
| Consn n a (Consn m b l) => n + m
821
match LeO 0 return nat with
823
| LeS n m (LeO x) => x + m
824
| LeS n m (LeS x y h) => n + x
831
| LeS n m (LeO x) => x + m
832
| LeS n m (LeS x y h) => n + x
837
match LeO 0 return nat with
839
| LeS n m (LeO x) => x + m
840
| LeS n m (LeS x y h) => m
846
| LeS n m (LeO x) => x + m
847
| LeS n m (LeS x y h) => m
852
(fun (n m : nat) (h : Le n m) =>
853
match h return nat with
858
Type (fun (n m : nat) (h : Le n m) => match h with
865
(fun (n m : nat) (h : Le n m) =>
866
match h return nat with
873
(fun (n m : nat) (h : Le n m) => match h with
880
(fun (n m : nat) (h : Le n m) =>
881
match h return (nat * nat) with
883
| LeS n m _ => (S n, S m)
888
(fun (n m : nat) (h : Le n m) =>
891
| LeS n m _ => (S n, S m)
895
Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) :=
896
match h in (Le n m) return (Le n (S m)) with
897
| LeO m' => LeO (S m')
898
| LeS n' m' h' => LeS n' (S m') (F n' m' h')
903
Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) :=
904
match h in (Le n m) return (Le n (S m)) with
905
| LeS n m h => LeS n (S m) (F n m h)
909
(* Rend la longueur de la liste *)
910
Definition length1 (n : nat) (l : listn n) :=
911
match l return nat with
912
| consn n _ (consn m _ _) => S (S m)
918
Definition length1 (n : nat) (l : listn n) :=
920
| consn n _ (consn m _ _) => S (S m)
926
Definition length2 (n : nat) (l : listn n) :=
927
match l return nat with
928
| consn n _ (consn m _ _) => S (S m)
935
Definition length2 (n : nat) (l : listn n) :=
937
| consn n _ (consn m _ _) => S (S m)
942
Definition length3 (n : nat) (l : listn n) :=
943
match l return nat with
944
| consn n _ (consn m _ l) => S n
952
Definition length3 (n : nat) (l : listn n) :=
954
| consn n _ (consn m _ l) => S n
960
Type match LeO 0 return nat with
964
Type match LeO 0 with
970
(fun (n m : nat) (h : Le n m) =>
971
match h return nat with
973
| LeS n m (LeO x) => x + m
974
| LeS n m (LeS x y h) => n + (m + (x + y))
979
(fun (n m : nat) (h : Le n m) =>
982
| LeS n m (LeO x) => x + m
983
| LeS n m (LeS x y h) => n + (m + (x + y))
987
match LeO 0 return nat with
989
| LeS n m (LeO x) => x + m
990
| LeS n m (LeS x y h) => n + (m + (x + y))
996
| LeS n m (LeO x) => x + m
997
| LeS n m (LeS x y h) => n + (m + (x + y))
1002
match LE_n 0 return nat with
1004
| LE_S m LE_n => 0 + m
1005
| LE_S m (LE_S y h) => 0 + m
1012
| LE_S m LE_n => 0 + m
1013
| LE_S m (LE_S y h) => 0 + m
1017
Type (fun (n m : nat) (h : Le n m) => match h with
1022
(fun (n m : nat) (h : Le n m) =>
1023
match h return nat with
1027
Type (fun (n m : nat) (h : Le n m) => match h with
1035
match niln return (nat -> nat) with
1036
| niln => fun _ : nat => 0
1037
| consn n a niln => fun _ : nat => 0
1038
| consn n a (consn m b l) => fun _ : nat => n + m
1045
| niln => fun _ : nat => 0
1046
| consn n a niln => fun _ : nat => 0
1047
| consn n a (consn m b l) => fun _ : nat => n + m
1051
(fun (A : Set) (n : nat) (l : Listn A n) =>
1052
match l return (nat -> nat) with
1053
| Niln => fun _ : nat => 0
1054
| Consn n a Niln => fun _ : nat => n
1055
| Consn n a (Consn m b l) => fun _ : nat => n + m
1059
(fun (A : Set) (n : nat) (l : Listn A n) =>
1061
| Niln => fun _ : nat => 0
1062
| Consn n a Niln => fun _ : nat => n
1063
| Consn n a (Consn m b l) => fun _ : nat => n + m
1066
(* Alsos tests for multiple _ patterns *)
1068
(fun (A : Set) (n : nat) (l : Listn A n) =>
1069
match l in (Listn _ n) return (Listn A n) with
1071
| Consn _ _ _ as b => b
1074
(** Horrible error message!
1076
Type [A:Set][n:nat][l:(Listn A n)]
1079
| ((Consn _ _ _ ) as b)=> b
1084
match niln in (listn n) return (listn n) with
1086
| consn _ _ _ as b => b
1091
match niln in (listn n) return (listn n) with
1097
(fun (n m : nat) (h : LE n m) =>
1098
match h return (nat -> nat) with
1099
| LE_n => fun _ : nat => n
1100
| LE_S m LE_n => fun _ : nat => n + m
1101
| LE_S m (LE_S y h) => fun _ : nat => m + y
1104
(fun (n m : nat) (h : LE n m) =>
1106
| LE_n => fun _ : nat => n
1107
| LE_S m LE_n => fun _ : nat => n + m
1108
| LE_S m (LE_S y h) => fun _ : nat => m + y
1113
(fun (n m : nat) (h : LE n m) =>
1114
match h return nat with
1116
| LE_S m LE_n => n + m
1117
| LE_S m (LE_S y LE_n) => n + m + y
1118
| LE_S m (LE_S y (LE_S y' h)) => n + m + (y + y')
1124
(fun (n m : nat) (h : LE n m) =>
1127
| LE_S m LE_n => n + m
1128
| LE_S m (LE_S y LE_n) => n + m + y
1129
| LE_S m (LE_S y (LE_S y' h)) => n + m + (y + y')
1134
(fun (n m : nat) (h : LE n m) =>
1135
match h return nat with
1137
| LE_S m LE_n => n + m
1138
| LE_S m (LE_S y h) => n + m + y
1143
(fun (n m : nat) (h : LE n m) =>
1146
| LE_S m LE_n => n + m
1147
| LE_S m (LE_S y h) => n + m + y
1152
match LeO 0 return nat with
1153
| LeS n m h => n + m
1157
Type (fun n m : nat => match LeO 0 with
1158
| LeS n m h => n + m
1162
Parameter test : forall n : nat, {0 <= n} + {False}.
1163
Type (fun n : nat => match test n return nat with
1169
Type (fun n : nat => match test n return nat with
1174
Type (fun n : nat => match test n with
1179
Parameter compare : forall n m : nat, {n < m} + {n = m} + {n > m}.
1181
match compare 0 0 return nat with
1183
(* k<i *) | inleft (left _) => 0
1184
(* k=i *) | inleft _ => 0
1185
(* k>i *) | inright _ => 0
1189
match compare 0 0 with
1191
(* k<i *) | inleft (left _) => 0
1192
(* k=i *) | inleft _ => 0
1193
(* k>i *) | inright _ => 0
1198
CoInductive SStream (A : Set) : (nat -> A -> Prop) -> Type :=
1200
forall (P : nat -> A -> Prop) (a : A),
1201
P 0 a -> SStream A (fun n : nat => P (S n)) -> SStream A P.
1205
(fun (P : nat -> B -> Prop) (x : SStream B P) =>
1206
match x return B with
1207
| scons _ a _ _ => a
1212
(fun (P : nat -> B -> Prop) (x : SStream B P) =>
1214
| scons _ a _ _ => a
1217
Type match (0, 0) return (nat * nat) with
1218
| (x, y) => (S x, S y)
1220
Type match (0, 0) return (nat * nat) with
1221
| (b, y) => (S b, S y)
1223
Type match (0, 0) return (nat * nat) with
1224
| (x, y) => (S x, S y)
1227
Type match (0, 0) with
1228
| (x, y) => (S x, S y)
1230
Type match (0, 0) with
1231
| (b, y) => (S b, S y)
1233
Type match (0, 0) with
1234
| (x, y) => (S x, S y)
1239
Parameter concat : forall A : Set, List A -> List A -> List A.
1242
match Nil nat, Nil nat return (List nat) with
1243
| Nil as b, x => concat nat b x
1244
| Cons _ _ as d, Nil as c => concat nat d c
1248
match Nil nat, Nil nat with
1249
| Nil as b, x => concat nat b x
1250
| Cons _ _ as d, Nil as c => concat nat d c
1255
Inductive redexes : Set :=
1256
| VAR : nat -> redexes
1257
| Fun : redexes -> redexes
1258
| Ap : bool -> redexes -> redexes -> redexes.
1260
Fixpoint regular (U : redexes) : Prop :=
1261
match U return Prop with
1263
| Fun V => regular V
1264
| Ap true (Fun _ as V) W => regular V /\ regular W
1265
| Ap true _ W => False
1266
| Ap false V W => regular V /\ regular W
1270
Type (fun n : nat => match n with
1279
forall n : nat, listn n -> forall m : nat, listn m -> listn (n + m).
1281
(fun (n : nat) (l : listn n) (m : nat) (l' : listn m) =>
1282
match l in (listn n), l' return (listn (n + m)) with
1284
| consn n a l'', x => consn (n + m) a (concat n l'' m x)
1288
(fun (x y z : nat) (H : x = y) (H0 : y = z) =>
1289
match H return (x = z) with
1291
match H0 in (_ = n) return (x = n) with
1296
Type (fun h : False => match h return False with
1299
Type (fun h : False => match h return True with
1302
Definition is_zero (n : nat) := match n with
1308
(fun (n : nat) (h : 0 = S n) =>
1309
match h in (_ = n) return (is_zero n) with
1313
Definition disc (n : nat) (h : 0 = S n) : False :=
1314
match h in (_ = n) return (is_zero n) with
1318
Definition nlength3 (n : nat) (l : listn n) :=
1322
| consn (S n) _ _ => S (S n)
1325
(* == Testing strategy elimintation predicate synthesis == *)
1334
Type match niln with
1335
| consn _ a niln => a
1342
Inductive wsort : Set :=
1345
Inductive TS : wsort -> Set :=
1347
| lift : TS ws -> TS ws.
1350
(fun (b : wsort) (M N : TS b) =>
1352
| lift M1, id => False
1358
(* ===================================================================== *)
1359
(* To test pattern matching over a non-dependent inductive type, but *)
1360
(* having constructors with some arguments that depend on others *)
1361
(* I.e. to test manipulation of elimination predicate *)
1362
(* ===================================================================== *)
1365
Parameter LTERM : nat -> Set.
1366
Inductive TERM : Type :=
1368
| oper : forall op : nat, LTERM op -> TERM.
1370
Parameter t1 t2 : TERM.
1375
| oper op1 l1, oper op2 l2 => False
1382
Require Import Peano_dec.
1384
Definition eq_prf := exists m : _, n = m.
1385
Parameter p : eq_prf.
1390
match eq_nat_dec c n with
1391
| right _ => refl_equal n
1392
| left y => (* c=n*) refl_equal n
1397
Parameter ordre_total : nat -> nat -> Prop.
1399
Parameter N_cla : forall N : nat, {N = 0} + {N = 1} + {N >= 2}.
1406
forall m : nat, 0 < m /\ m <= N /\ ordre_total n m /\ 0 < n /\ n < N}.
1411
| inright H => match exist_U2 N H with
1419
(* ============================================== *)
1420
(* To test compilation of dependent case *)
1421
(* Nested patterns *)
1422
(* ============================================== *)
1424
(* == To test that terms named with AS are correctly absolutized before
1425
substitution in rhs == *)
1429
match n return nat with
1432
| S (S n1) as N => N
1438
match niln in (listn n) return Prop with
1440
| consn (S O) _ _ => False
1445
match niln in (listn n) return Prop with
1447
| consn (S (S O)) _ _ => False
1453
match LeO 0 as h in (Le n m) return nat with
1455
| LeS (S x) _ _ => x
1460
match LeO 0 as h in (Le n m) return nat with
1462
| LeS (S x) (S y) _ => x
1467
match LeO 0 as h in (Le n m) return nat with
1469
| LeS (S x as b) (S y) _ => b
1475
Parameter ff : forall n m : nat, n <> m -> S n <> S m.
1476
Parameter discr_r : forall n : nat, 0 <> S n.
1477
Parameter discr_l : forall n : nat, S n <> 0.
1481
match n return (n = 0 \/ n <> 0) with
1482
| O => or_introl (0 <> 0) (refl_equal 0)
1483
| S x => or_intror (S x = 0) (discr_l x)
1487
Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
1488
match n, m return (n = m \/ n <> m) with
1489
| O, O => or_introl (0 <> 0) (refl_equal 0)
1490
| O, S x => or_intror (0 = S x) (discr_r x)
1491
| S x, O => or_intror _ (discr_l x)
1493
match eqdec x y return (S x = S y \/ S x <> S y) with
1494
| or_introl h => or_introl (S x <> S y) (f_equal S h)
1495
| or_intror h => or_intror (S x = S y) (ff x y h)
1501
Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
1502
match n return (forall m : nat, n = m \/ n <> m) with
1505
match m return (0 = m \/ 0 <> m) with
1506
| O => or_introl (0 <> 0) (refl_equal 0)
1507
| S x => or_intror (0 = S x) (discr_r x)
1511
match m return (S x = m \/ S x <> m) with
1512
| O => or_intror (S x = 0) (discr_l x)
1514
match eqdec x y return (S x = S y \/ S x <> S y) with
1515
| or_introl h => or_introl (S x <> S y) (f_equal S h)
1516
| or_intror h => or_intror (S x = S y) (ff x y h)
1522
Inductive empty : forall n : nat, listn n -> Prop :=
1523
intro_empty : empty 0 niln.
1526
inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l).
1529
(fun (n : nat) (l : listn n) =>
1530
match l in (listn n) return (empty n l \/ ~ empty n l) with
1531
| niln => or_introl (~ empty 0 niln) intro_empty
1532
| consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
1536
Parameter ff : forall n m : nat, n <> m -> S n <> S m.
1537
Parameter discr_r : forall n : nat, 0 <> S n.
1538
Parameter discr_l : forall n : nat, S n <> 0.
1542
match n return (n = 0 \/ n <> 0) with
1543
| O => or_introl (0 <> 0) (refl_equal 0)
1544
| S x => or_intror (S x = 0) (discr_l x)
1548
Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
1549
match n, m return (n = m \/ n <> m) with
1550
| O, O => or_introl (0 <> 0) (refl_equal 0)
1551
| O, S x => or_intror (0 = S x) (discr_r x)
1552
| S x, O => or_intror _ (discr_l x)
1554
match eqdec x y return (S x = S y \/ S x <> S y) with
1555
| or_introl h => or_introl (S x <> S y) (f_equal S h)
1556
| or_intror h => or_intror (S x = S y) (ff x y h)
1561
Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
1562
match n return (forall m : nat, n = m \/ n <> m) with
1565
match m return (0 = m \/ 0 <> m) with
1566
| O => or_introl (0 <> 0) (refl_equal 0)
1567
| S x => or_intror (0 = S x) (discr_r x)
1571
match m return (S x = m \/ S x <> m) with
1572
| O => or_intror (S x = 0) (discr_l x)
1574
match eqdec x y return (S x = S y \/ S x <> S y) with
1575
| or_introl h => or_introl (S x <> S y) (f_equal S h)
1576
| or_intror h => or_intror (S x = S y) (ff x y h)
1582
(* ================================================== *)
1583
(* Pour tester parametres *)
1584
(* ================================================== *)
1587
Inductive Empty (A : Set) : List A -> Prop :=
1588
intro_Empty : Empty A (Nil A).
1591
inv_Empty : forall (A : Set) (a : A) (x : List A), ~ Empty A (Cons A a x).
1595
match Nil nat as l return (Empty nat l \/ ~ Empty nat l) with
1596
| Nil => or_introl (~ Empty nat (Nil nat)) (intro_Empty nat)
1597
| Cons a y => or_intror (Empty nat (Cons nat a y)) (inv_Empty nat a y)
1601
(* ================================================== *)
1602
(* Sur les listes *)
1603
(* ================================================== *)
1606
Inductive empty : forall n : nat, listn n -> Prop :=
1607
intro_empty : empty 0 niln.
1610
inv_empty : forall (n a : nat) (l : listn n), ~ empty (S n) (consn n a l).
1613
(fun (n : nat) (l : listn n) =>
1614
match l in (listn n) return (empty n l \/ ~ empty n l) with
1615
| niln => or_introl (~ empty 0 niln) intro_empty
1616
| consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
1619
(* ===================================== *)
1620
(* Test parametros: *)
1621
(* ===================================== *)
1623
Inductive eqlong : List nat -> List nat -> Prop :=
1625
forall (n m : nat) (x y : List nat),
1626
eqlong x y -> eqlong (Cons nat n x) (Cons nat m y)
1627
| eql_nil : eqlong (Nil nat) (Nil nat).
1630
Parameter V1 : eqlong (Nil nat) (Nil nat) \/ ~ eqlong (Nil nat) (Nil nat).
1633
forall (a : nat) (x : List nat),
1634
eqlong (Nil nat) (Cons nat a x) \/ ~ eqlong (Nil nat) (Cons nat a x).
1637
forall (a : nat) (x : List nat),
1638
eqlong (Cons nat a x) (Nil nat) \/ ~ eqlong (Cons nat a x) (Nil nat).
1641
forall (a : nat) (x : List nat) (b : nat) (y : List nat),
1642
eqlong (Cons nat a x) (Cons nat b y) \/
1643
~ eqlong (Cons nat a x) (Cons nat b y).
1646
match Nil nat as x, Nil nat as y return (eqlong x y \/ ~ eqlong x y) with
1648
| Nil, Cons a x => V2 a x
1649
| Cons a x, Nil => V3 a x
1650
| Cons a x, Cons b y => V4 a x b y
1655
(fun x y : List nat =>
1656
match x, y return (eqlong x y \/ ~ eqlong x y) with
1658
| Nil, Cons a x => V2 a x
1659
| Cons a x, Nil => V3 a x
1660
| Cons a x, Cons b y => V4 a x b y
1664
(* ===================================== *)
1667
forall n : nat, listn n -> forall m : nat, listn m -> Prop :=
1669
forall (n m : nat) (x : listn n) (y : listn m) (a b : nat),
1670
Eqlong n x m y -> Eqlong (S n) (consn n a x) (S m) (consn m b y)
1671
| Eql_niln : Eqlong 0 niln 0 niln.
1674
Parameter W1 : Eqlong 0 niln 0 niln \/ ~ Eqlong 0 niln 0 niln.
1677
forall (n a : nat) (x : listn n),
1678
Eqlong 0 niln (S n) (consn n a x) \/ ~ Eqlong 0 niln (S n) (consn n a x).
1681
forall (n a : nat) (x : listn n),
1682
Eqlong (S n) (consn n a x) 0 niln \/ ~ Eqlong (S n) (consn n a x) 0 niln.
1685
forall (n a : nat) (x : listn n) (m b : nat) (y : listn m),
1686
Eqlong (S n) (consn n a x) (S m) (consn m b y) \/
1687
~ Eqlong (S n) (consn n a x) (S m) (consn m b y).
1691
niln as x in (listn n), niln as y in (listn m)
1692
return (Eqlong n x m y \/ ~ Eqlong n x m y)
1695
| niln, consn n a x => W2 n a x
1696
| consn n a x, niln => W3 n a x
1697
| consn n a x, consn m b y => W4 n a x m b y
1702
(fun (n m : nat) (x : listn n) (y : listn m) =>
1704
x in (listn n), y in (listn m)
1705
return (Eqlong n x m y \/ ~ Eqlong n x m y)
1708
| niln, consn n a x => W2 n a x
1709
| consn n a x, niln => W3 n a x
1710
| consn n a x, consn m b y => W4 n a x m b y
1716
forall (n a : nat) (x : listn n), ~ Eqlong 0 niln (S n) (consn n a x).
1719
forall (n a : nat) (x : listn n), ~ Eqlong (S n) (consn n a x) 0 niln.
1722
forall (n a : nat) (x : listn n) (m b : nat) (y : listn m),
1723
~ Eqlong n x m y -> ~ Eqlong (S n) (consn n a x) (S m) (consn m b y).
1727
Fixpoint Eqlongdec (n : nat) (x : listn n) (m : nat)
1728
(y : listn m) {struct x} : Eqlong n x m y \/ ~ Eqlong n x m y :=
1730
x in (listn n), y in (listn m)
1731
return (Eqlong n x m y \/ ~ Eqlong n x m y)
1733
| niln, niln => or_introl (~ Eqlong 0 niln 0 niln) Eql_niln
1734
| niln, consn n a x as L => or_intror (Eqlong 0 niln (S n) L) (Inv_r n a x)
1735
| consn n a x as L, niln => or_intror (Eqlong (S n) L 0 niln) (Inv_l n a x)
1736
| consn n a x as L1, consn m b y as L2 =>
1739
return (Eqlong (S n) L1 (S m) L2 \/ ~ Eqlong (S n) L1 (S m) L2)
1742
or_introl (~ Eqlong (S n) L1 (S m) L2) (Eql_cons n m x y a b h)
1744
or_intror (Eqlong (S n) L1 (S m) L2) (Nff n a x m b y h)
1748
(* ============================================== *)
1749
(* To test compilation of dependent case *)
1750
(* Multiple Patterns *)
1751
(* ============================================== *)
1752
Inductive skel : Type :=
1754
| PROD : skel -> skel -> skel.
1756
Parameter Can : skel -> Type.
1757
Parameter default_can : forall s : skel, Can s.
1760
(fun s1 s2 s1 s2 : skel =>
1761
match s1, s2 return (Can s1) with
1762
| PROP, PROP => default_can PROP
1763
| PROD x y, PROP => default_can (PROD x y)
1764
| PROD x y, _ => default_can (PROD x y)
1765
| PROP, _ => default_can PROP
1768
(* to test bindings in nested Cases *)
1769
(* ================================ *)
1770
Inductive Pair : Set :=
1772
| pcons : Pair -> Pair -> Pair.
1777
| pcons _ x => match q with
1778
| pcons _ (pcons _ x) => True
1790
| pcons _ (pcons _ x) =>
1792
| pcons _ (pcons _ (pcons _ x)) => x
1801
(fun (n : nat) (l : listn (S n)) =>
1802
match l in (listn z) return (listn (pred z)) with
1805
match l in (listn m) return (listn m) with
1813
(* Test de la syntaxe avec nombres *)
1814
Require Import Arith.
1815
Type (fun n => match n with
1820
Require Import ZArith.
1821
Type (fun n => match n with
added
removed
test-suite/success/Cases.v
