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
|
Require Import ssreflect.
Section foo.
Variable A : Type.
Record bar (X : Type) := mk_bar {
a : X * A;
b : A;
c := (a,7);
_ : X;
_ : X
}.
Inductive baz (X : Type) (Y : Type) : nat -> Type :=
| K1 x (e : 0=1) (f := 3) of x=x:>X : baz X Y O
| K2 n of n=n & baz X nat 0 : baz X Y (n+1).
Axiom Q : nat -> Prop.
Axiom Qx : forall x, Q x.
Axiom my_ind :
forall P : nat -> Prop, P O -> (forall n m (w : P n /\ P m), P (n+m)) ->
forall w, P w.
Lemma test x : bar nat -> baz nat nat x -> forall n : nat, Q n.
Proof.
(* record *)
move => [^~ _ccc ].
Check (refl_equal _ : c_ccc = (a_ccc, 7)).
(* inductive *)
move=> [^ xxx_ ].
Check (refl_equal _ : xxx_f = 3).
by [].
Check (refl_equal _ : xxx_n = xxx_n).
(* eliminator *)
elim/my_ind => [^ wow_ ].
exact: Qx 0.
Check (wow_w : Q wow_n /\ Q wow_m).
exact: Qx (wow_n + wow_m).
Qed.
Arguments mk_bar A x y z w : rename.
Arguments K1 A B a b c : rename.
Lemma test2 x : bar nat -> baz nat nat x -> forall n : nat, Q n.
Proof.
move=> [^~ _ccc ].
Check (refl_equal _ : c_ccc = (x_ccc, 7)).
move=> [^ xxx_ ].
Check (refl_equal _ : xxx_f = 3).
by [].
Check (refl_equal _ : xxx_n = xxx_n).
Abort.
End foo.
|
