From 164c6861860e6b52818c031f901ffeff91fca16a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 26 Jan 2016 16:56:33 +0100 Subject: Imported Upstream version 8.5 --- test-suite/success/keyedrewrite.v | 37 +++++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) (limited to 'test-suite/success/keyedrewrite.v') diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v index bbe9d4bf..5b0502cf 100644 --- a/test-suite/success/keyedrewrite.v +++ b/test-suite/success/keyedrewrite.v @@ -22,3 +22,40 @@ 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. \ No newline at end of file -- cgit v1.2.3