1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
|
(* -*- mode: coq; coq-prog-args: ("-noinit" "-indices-matter") -*- *)
(* This file tests the discriminate tactic compatibility with HoTT.
The first part of the file will setup a mini HoTT environment.
Afterwards a number of tests are performed. The tests are basically
copied from the Discriminate.v test file. *)
Unset Elimination Schemes.
Set Universe Polymorphism.
Declare ML Module "ltac_plugin".
Global Set Default Proof Mode "Classic".
Notation "x -> y" := (forall (_:x), y) (at level 99, right associativity, y at level 200).
Cumulative Variant paths {A} (a:A) : A -> Type
:= idpath : paths a a.
Arguments idpath {A a} , [A] a.
Scheme paths_ind := Induction for paths Sort Type.
Arguments paths_ind [A] a P f y p.
Notation "x = y :> A" := (@paths A x y) (at level 70, y at next level, no associativity).
Notation "x = y" := (x = y :>_) (at level 70, no associativity).
Register paths as core.identity.type.
Register idpath as core.identity.refl.
Register paths_ind as core.identity.ind.
Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
:= match p with idpath => idpath end.
Arguments inverse {A x y} p : simpl nomatch.
Register inverse as core.identity.sym.
Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
match p, q with idpath, idpath => idpath end.
Arguments concat {A x y z} p q : simpl nomatch.
Register concat as core.identity.trans.
Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
:= match p with idpath => idpath end.
Arguments ap {A B} f {x y} p.
Register ap as core.identity.congr.
Variant Empty : Type :=.
Register Empty as core.False.type.
Variant Unit : Type := tt.
Register Unit as core.True.type.
Register tt as core.True.I.
Variant Bool : Type := true | false.
Inductive nat : Type := O | S (n:nat).
(*********** Test discriminate tactic below. ***************)
Goal O = S O -> Empty.
discriminate 1.
Qed.
Goal forall H : O = S O, H = H.
discriminate H.
Qed.
Goal O = S O -> Unit.
intros. discriminate H. Qed.
Goal O = S O -> Unit.
intros. Ltac g x := discriminate x. g H. Qed.
Goal (forall x y : nat, x = y -> x = S y) -> Unit.
intros.
try discriminate (H O) || exact tt.
Qed.
Goal (forall x y : nat, x = y -> x = S y) -> Unit.
intros. ediscriminate (H O). instantiate (1:=O). Abort.
(* Check discriminate on types with local definitions *)
Inductive A := B (T := Unit) (x y : Bool) (z := x).
Goal forall x y, B x true = B y false -> Empty.
discriminate.
Qed.
|
