blob: b06718251e7fa07ff19c3d91ac8dd59ea07c7684 (
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
|
(* Check that dependent rewrite applies on arbitrary terms *)
Inductive listn : nat -> Set :=
| niln : listn 0
| consn : forall n : nat, nat -> listn n -> listn (S n).
Axiom
ax :
forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)),
existS _ (n + n') l = existS _ (n' + n) l'.
Lemma lem :
forall (n n' : nat) (l : listn (n + n')) (l' : listn (n' + n)),
n + n' = n' + n /\ existT _ (n + n') l = existT _ (n' + n) l'.
Proof.
intros n n' l l'.
dependent rewrite (ax n n' l l').
split; reflexivity.
Qed.
(* Used to raise an anomaly instead of an error in 8.1 *)
(* Submitted by Y. Makarov *)
Parameter N : Set.
Parameter E : N -> N -> Prop.
Axiom e : forall (A : Set) (EA : A -> A -> Prop) (a : A), EA a a.
Theorem th : forall x : N, E x x.
intro x. try rewrite e.
Abort.
(* Behavior of rewrite wrt conversion *)
Require Import Arith.
Goal forall n, 0 + n = n -> True.
intros n H.
rewrite plus_0_l in H.
Abort.
(* Dependent rewrite from left-to-right *)
Lemma l1 :
forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H.
intros x y H P H0.
rewrite H.
rewrite H in H0.
assumption.
Qed.
(* Dependent rewrite from right-to-left *)
Lemma l2 :
forall x y (H:x = y:>nat) (P:forall x y, x=y -> Type), P x y H -> P x y H.
intros x y H P H0.
rewrite <- H.
rewrite <- H in H0.
assumption.
Qed.
(* Check dependent rewriting with non-symmetric equalities *)
Lemma l3:forall x (H:eq_true x) (P:forall x, eq_true x -> Type), P x H -> P x H.
intros x H P H0.
rewrite H.
rewrite H in H0.
assumption.
Qed.
|
