aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/keyedrewrite.v
blob: 5638a7d3eb818b8349cbf61d3ad66b2eb1d000c6 (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
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 Omega.

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.