aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/setoid_unif.v
blob: 912596b4a3e3ac08a7f217ee8dcead9e828e4169 (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
(* An example of unification in rewrite which uses eager substitution
   of metas (provided by Pierre-Marie).

   Put in the test suite as an indication of what the use metas
   eagerly flag provides, even though the concrete cases that use it
   are seldom. Today supported thanks to a new flag for using evars
   eagerly, after this variant of setoid rewrite started to use clause
   environments based on evars (fbbe491cfa157da627) *)

Require Import Setoid.

Parameter elt : Type.
Parameter T : Type -> Type.
Parameter empty : forall A, T A.
Parameter MapsTo : forall A : Type, elt -> A -> T A -> Prop.

(* Definition In A x t := exists e, MapsTo A x e t. *)
Axiom In : forall A, A -> T A -> Prop.
Axiom foo : forall A x, In A x (empty A) <-> False.

Record R := { t : T unit; s : unit }.
Definition Empty := {| t := empty unit; s := tt |}.

Goal forall x, ~ In _ x (t Empty).
Proof.
intros x.
rewrite foo.