blob: fbccf049c0557dd2b3a4c6c4323489910eea261c (
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
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
|
Require Import NZAxioms.
Module NZBasePropFunct (Import NZAxiomsMod : NZAxiomsSig).
Open Local Scope NatIntScope.
Theorem NZneq_symm : forall n m : NZ, n ~= m -> m ~= n.
Proof.
intros n m H1 H2; symmetry in H2; false_hyp H2 H1.
Qed.
Theorem NZE_stepl : forall x y z : NZ, x == y -> x == z -> z == y.
Proof.
intros x y z H1 H2; now rewrite <- H1.
Qed.
Declare Left Step NZE_stepl.
(* The right step lemma is just the transitivity of NZE *)
Declare Right Step (proj1 (proj2 NZE_equiv)).
Theorem NZsucc_inj : forall n1 n2 : NZ, S n1 == S n2 -> n1 == n2.
Proof.
intros n1 n2 H.
apply NZpred_wd in H. now do 2 rewrite NZpred_succ in H.
Qed.
(* The following theorem is useful as an equivalence for proving
bidirectional induction steps *)
Theorem NZsucc_inj_wd : forall n1 n2 : NZ, S n1 == S n2 <-> n1 == n2.
Proof.
intros; split.
apply NZsucc_inj.
apply NZsucc_wd.
Qed.
Theorem NZsucc_inj_wd_neg : forall n m : NZ, S n ~= S m <-> n ~= m.
Proof.
intros; now rewrite NZsucc_inj_wd.
Qed.
(* We cannot prove that the predecessor is injective, nor that it is
left-inverse to the successor at this point *)
Section CentralInduction.
Variable A : NZ -> Prop.
(* FIXME: declaring "A : predicate NZ" leads to the error during the
declaration of the morphism below because the "predicate NZ" is not
recognized as a type of function. Maybe it should do "eval hnf" or
something like this. The same goes for "relation". *)
Hypothesis A_wd : predicate_wd NZE A.
Add Morphism A with signature NZE ==> iff as A_morph.
Proof A_wd.
Theorem NZcentral_induction :
forall z : NZ, A z ->
(forall n : NZ, A n <-> A (S n)) ->
forall n : NZ, A n.
Proof.
intros z Base Step; revert Base; pattern z; apply NZinduction.
solve_predicate_wd.
intro; now apply NZinduction.
intro; pose proof (Step n); tauto.
Qed.
End CentralInduction.
Tactic Notation "NZinduct" ident(n) :=
induction_maker n ltac:(apply NZinduction).
Tactic Notation "NZinduct" ident(n) constr(u) :=
induction_maker n ltac:(apply NZcentral_induction with (z := u)).
End NZBasePropFunct.
(*
Local Variables:
tags-file-name: "~/coq/trunk/theories/Numbers/TAGS"
End:
*)
|
