aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/subtac/test/id.v
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.