-
Notifications
You must be signed in to change notification settings - Fork 4
/
Copy pathnatsind.v
66 lines (55 loc) · 1.27 KB
/
natsind.v
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
Section InductionPrinciple.
Variable P : nat -> Type.
Require Import Omega.
Definition nat_xrect_aux:
(forall n, (forall m, m<n -> P m) -> P n) ->
forall n, (forall m, m<n -> P m).
Proof.
induction n as [|n IHn].
- intros m H.
omega.
- intros m H.
apply X.
intros m0 H0.
apply IHn.
omega.
Qed.
Definition weaken:
(forall n, (forall m, m<n -> P m)) -> (forall n, P n).
Proof.
intros X n.
apply (X (S n) n).
omega.
Qed.
Theorem nat_xrect:
(forall n, (forall m, m<n -> P m) -> P n) -> forall n, P n.
Proof.
intros X n.
apply weaken.
apply nat_xrect_aux.
assumption.
Qed.
End InductionPrinciple.
Section EInductionPrinciple.
Require Import erasable.
Import ErasableNotation.
Notation EN := (##nat).
Definition Elt := liftP2 lt.
Theorem Elt_wf : well_founded Elt.
Proof.
intros y.
unerase.
induction y as [y H] using nat_xrect.
constructor.
intros ? (x & ? & ? & ? & ?).
simplify_hyps.
apply H.
assumption.
Qed.
Variable P : EN -> Type.
Definition enat_xrect := well_founded_induction_type Elt_wf.
End EInductionPrinciple.
Extraction Inline weaken.
Extraction Inline nat_xrect_aux.
Extraction Inline nat_xrect.
Extraction Inline enat_xrect.