blob: 9ae1108817cd1f32395b22c2f02519fee6245e49 (
plain)
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
|
Require Coq.Arith.Arith.
Require Import Coq.subtac.Utils.
Program Fixpoint id (n : nat) : { x : nat | x = n } :=
match n with
| O => O
| S p => S (id p)
end.
intros ; auto.
pose (subset_simpl (id p)).
simpl in e.
unfold p0.
rewrite e.
auto.
Defined.
Check id.
Print id.
Extraction id.
Axiom le_gt_dec : forall n m, { n <= m } + { n > m }.
Require Import Omega.
Program Fixpoint id_if (n : nat) { wf n lt }: { x : nat | x = n } :=
if le_gt_dec n 0 then 0
else S (id_if (pred n)).
intros.
auto with arith.
intros.
pose (subset_simpl (id_if (pred n))).
simpl in e.
rewrite e.
induction n ; auto with arith.
Defined.
Print id_if_instance.
Extraction id_if_instance.
Notation "( x & y )" := (@existS _ _ x y) : core_scope.
Program Definition testsig ( a : nat ) : { x : nat & { y : nat | x = y }} :=
(a & a).
intros.
auto.
Qed.
|
