diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:04:54 +0100 |
commit | 39efc41237ec906226a3a53d7396d51173495204 (patch) | |
tree | 87cd58d72d43469d2a2a0a127c1060d7c9e0206b /test-suite/success/setoid_test.v | |
parent | 5fe4ac437bed43547b3695664974f492b55cb553 (diff) | |
parent | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff) |
Remove non-DFSG contentsupstream/8.4_beta+dfsg
Diffstat (limited to 'test-suite/success/setoid_test.v')
-rw-r--r-- | test-suite/success/setoid_test.v | 35 |
1 files changed, 35 insertions, 0 deletions
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v index 033b3f48..19693d70 100644 --- a/test-suite/success/setoid_test.v +++ b/test-suite/success/setoid_test.v @@ -130,3 +130,38 @@ intros f0 Q H. setoid_rewrite H. tauto. Qed. + +(** Check proper refreshing of the lemma application for multiple + different instances in a single setoid rewrite. *) + +Section mult. + Context (fold : forall {A} {B}, (A -> B) -> A -> B). + Context (add : forall A, A -> A). + Context (fold_lemma : forall {A B f} {eqA : relation B} x, eqA (fold A B f (add A x)) (fold _ _ f x)). + Context (ab : forall B, A -> B). + Context (anat : forall A, nat -> A). + +Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))). +Proof. intros. + setoid_rewrite fold_lemma. + change (fold A A (fun x0 : A => ab A x0) x = anat A (fold A nat (ab nat) x)). +Abort. + +End mult. + +(** Current semantics for rewriting with typeclass constraints in the lemma + does not fix the instance at the first unification, use [at], or simply rewrite for + this semantics. *) + +Require Import Arith. + +Class Foo (A : Type) := {foo_neg : A -> A ; foo_prf : forall x : A, x = foo_neg x}. +Instance: Foo nat. admit. Defined. +Instance: Foo bool. admit. Defined. + +Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. +Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort. + +Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y. +Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort. + |