-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathHypotheses.v
127 lines (107 loc) · 1.94 KB
/
Hypotheses.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
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
Add LoadPath "coq".
Require Import Arith NPeano.
Require Import Patcher.Patch.
Require Import String.
Open Scope string_scope.
(*
* Changes in hypotheses of inductive proofs
*)
Theorem old1:
forall (n m p : nat),
n < m ->
m <= p ->
n <= p.
Proof.
intros. induction H0.
- auto with arith.
- apply le_S. auto.
Qed.
Theorem new1:
forall (n m p : nat),
n <= m ->
m <= p ->
n <= p.
Proof.
intros. induction H0.
- auto with arith.
- apply le_S. auto.
Qed.
Patch Proof old1 new1 as patch1.
Theorem testPatch1:
forall n m,
n < m ->
n <= m.
Proof.
exact patch1.
Qed.
Theorem old2:
forall (n m p : nat),
n < m ->
m <= p ->
n <= p.
Proof.
intros. apply PeanoNat.Nat.lt_le_incl in H. induction H0.
- auto with arith.
- apply le_S. auto.
Qed.
Definition new2 := new1.
Patch Proof old2 new2 as patch2.
Theorem testPatch2:
forall n m,
n < m ->
n <= m.
Proof.
exact patch2.
Qed.
Theorem old3 :
forall (n m p : nat),
n < m + 1 ->
m <= p ->
n <= p.
Proof.
intros. rewrite plus_comm in H. induction H0.
- auto with arith.
- constructor. apply IHle.
Qed.
Definition new3 := new1.
Patch Proof old3 new3 as patch3.
Theorem testPatch3:
forall n m,
n < m + 1 ->
n <= m.
Proof.
exact patch3.
Qed.
(* --- Invertible changes in hypotheses --- *)
Definition old4 := old3.
Theorem new4 :
forall (n m p : nat),
n < S m ->
m <= p ->
n <= p.
Proof.
intros. induction H0.
- auto with arith.
- constructor. apply IHle.
Qed.
(*
* This doesn't work yet. To fix it, we need to check on primitive differencing
* to see if it's making simplifying assumptions about how to difference
* in this case.
*)
Patch Proof old4 new4 as patch4.
Patch Proof new4 old4 as patch4_inv.
Theorem testPatch4:
forall n m,
n < m + 1 ->
n < S m.
Proof.
exact patch4.
Qed.
Theorem testPatch4_inv:
forall n m,
n < S m ->
n < m + 1.
Proof.
exact patch4_inv.
Qed.