From 61dc740ed1c3780cccaec00d059a28f0d31d0052 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 4 Jun 2012 12:07:52 +0200
Subject: Imported Upstream version 8.4~gamma0+really8.4beta2

---
 test-suite/success/evars.v | 70 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 70 insertions(+)

(limited to 'test-suite/success/evars.v')

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 2f1ec757..e6088091 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -309,3 +309,73 @@ Definition k6
 Definition k7
   (e:forall P : nat -> Prop, (exists n : nat, let n' := n in P n') -> nat)
   (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
+
+(* An example that uses materialize_evar under binders *)
+(* Extracted from bigop.v in the mathematical components library *)
+
+Section Bigop.
+
+Variable bigop : forall R I: Type,
+  R -> (R -> R -> R) -> list I -> (I->Prop) -> (I -> R) -> R.
+
+Hypothesis eq_bigr :
+forall (R : Type) (idx : R) (op : R -> R -> R)
+       (I : Type) (r : list I) (P : I -> Prop) (F1 F2 : I -> R),
+       (forall i : I, P i -> F1 i = F2 i) ->
+       bigop R I idx op r (fun i : I => P i) (fun i : I => F1 i) = idx.
+
+Hypothesis big_tnth :
+forall (R : Type) (idx : R) (op : R -> R -> R)
+     (I : Type) (r : list I) (P : I -> Prop) (F : I -> R),
+     bigop R I idx op r (fun i : I => P i) (fun i : I => F i) = idx.
+
+Hypothesis big_tnth_with_letin :
+forall (R : Type) (idx : R) (op : R -> R -> R)
+     (I : Type) (r : list I) (P : I -> Prop) (F : I -> R),
+     bigop R I idx op r (fun i : I => let i:=i in P i) (fun i : I => F i) = idx.
+
+Variable R : Type.
+Variable idx : R.
+Variable op : R -> R -> R.
+Variable I : Type.
+Variable J : Type.
+Variable rI : list I.
+Variable rJ : list J.
+Variable xQ : J -> Prop.
+Variable P : I -> Prop.
+Variable Q : I -> J -> Prop.
+Variable F : I -> J -> R.
+
+(* Check unification under binders *)
+
+Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth _ _ _ _ rI _ _))
+  : (bigop R J idx op rJ
+        (fun j : J => let k:=j in xQ k)
+        (fun j : J => let k:=j in 
+         bigop R I idx
+           op rI
+           (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx.
+
+(* Check also with let-in *)
+
+Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth_with_letin _ _ _ _ rI _ _))
+  : (bigop R J idx op rJ
+        (fun j : J => let k:=j in xQ k)
+        (fun j : J => let k:=j in 
+         bigop R I idx
+           op rI
+           (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx.
+
+End Bigop.
+
+(* Check the use of (at least) an heuristic to solve problems of the form
+   "?x[t] = ?y" where ?y occurs in t without easily knowing if ?y can
+   eventually be erased in t *)
+
+Section evar_evar_occur.
+  Variable id : nat -> nat.
+  Variable f : forall x, id x = 0 -> id x = 0 -> x = 1 /\ x = 2.
+  Variable g : forall y, id y = 0 /\ id y = 0.
+  (* Still evars in the resulting type, but constraints should be solved *)
+  Check match g _ with conj a b => f _ a b end.
+End evar_evar_occur.
-- 
cgit v1.2.3