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
|
Set Keyed Unification.
Section foo.
Variable f : nat -> nat.
Definition g := f.
Variable lem : g 0 = 0.
Goal f 0 = 0.
Proof.
Fail rewrite lem.
Abort.
Declare Equivalent Keys @g @f.
(** Now f and g are considered equivalent heads for subterm selection *)
Goal f 0 = 0.
Proof.
rewrite lem.
reflexivity.
Qed.
Print Equivalent Keys.
End foo.
Require Import Arith List.
Definition G {A} (f : A -> A -> A) (x : A) := f x x.
Lemma list_foo A (l : list A) : G (@app A) (l ++ nil) = G (@app A) l.
Proof. unfold G; rewrite app_nil_r; reflexivity. Qed.
(* Bundled version of a magma *)
Structure magma := Magma { b_car :> Type; op : b_car -> b_car -> b_car }.
Arguments op {_} _ _.
(* Instance for lists *)
Canonical Structure list_magma A := Magma (list A) (@app A).
(* Basically like list_foo, but now uses the op projection instead of app for
the argument of G *)
Lemma test1 A (l : list A) : G op (l ++ nil) = G op l.
(* Ensure that conversion of terms with evars is allowed once a keyed candidate unifier is found *)
rewrite -> list_foo.
reflexivity.
Qed.
(* Basically like list_foo, but now uses the op projection for everything *)
Lemma test2 A (l : list A) : G op (op l nil) = G op l.
Proof.
rewrite ->list_foo.
reflexivity.
Qed.
Require Import Bool.
Set Keyed Unification.
Lemma test b : b && true = b.
Fail rewrite andb_true_l.
Admitted.
|
