From a369ebb35a13ea8b71d3960637937e6cde41211a Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 7 Dec 2016 12:37:51 +0100
Subject: better test for primitive projections

---
 mathcomp/ssrtest/primproj.v | 97 ++++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 95 insertions(+), 2 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssrtest/primproj.v b/mathcomp/ssrtest/primproj.v
index 25afb28..90591d7 100644
--- a/mathcomp/ssrtest/primproj.v
+++ b/mathcomp/ssrtest/primproj.v
@@ -1,6 +1,38 @@
-From mathcomp Require Import ssreflect.
 
 
+Require Import Setoid.
+Set Primitive Projections.
+
+
+Module CoqBug.
+Record foo A := Foo { foo_car : A }.
+
+Definition bar : foo _ := Foo nat 10.
+
+Variable alias : forall A, foo A -> A.
+
+Parameter e : @foo_car = alias.
+
+Goal foo_car _ bar = alias _ bar.
+Proof.
+(* Coq equally fails *)
+Fail rewrite -> e.
+Fail rewrite e at 1.
+Fail setoid_rewrite e.
+Fail setoid_rewrite e at 1.
+Set Keyed Unification.
+Fail rewrite -> e.
+Fail rewrite e at 1.
+Fail setoid_rewrite e.
+Fail setoid_rewrite e at 1.
+Admitted.
+
+End CoqBug.
+
+(* ----------------------------------------------- *)
+
+From mathcomp Require Import ssreflect.
+
 Set Primitive Projections.
 
 Module T1.
@@ -10,6 +42,7 @@ Record foo A := Foo { foo_car : A }.
 Definition bar : foo _ := Foo nat 10.
 
 Goal foo_car _ bar = 10.
+Proof.
 match goal with
 | |- foo_car _ bar = 10 => idtac
 end.
@@ -48,13 +81,73 @@ Record foo {A} := Foo { foo_car : A }.
 Definition bar : foo := Foo nat 10.
 
 Goal foo_car bar = 10.
+Proof.
 rewrite -[foo_car _]/(id _).
 match goal with |- id _ = 10 => idtac end.
 Admitted.
 
 Goal foo_car bar = 10.
+Proof.
 set x := foo_car _.
 match goal with |- x = 10 => idtac end.
 Admitted.
 
-End T3.
\ No newline at end of file
+End T3.
+
+Module T4.
+
+Inductive seal {A} (f : A) := { unseal : A; seal_eq : unseal = f }.
+Arguments unseal {_ _} _.
+Arguments seal_eq {_ _} _.
+
+Record uPred : Type := IProp { uPred_holds :> Prop }.
+
+Definition uPred_or_def (P Q : uPred) : uPred :=
+  {| uPred_holds := P \/ Q |}.
+Definition uPred_or_aux : seal (@uPred_or_def). by eexists. Qed.
+Definition uPred_or := unseal uPred_or_aux.
+Definition uPred_or_eq: @uPred_or = @uPred_or_def := seal_eq uPred_or_aux.
+
+Lemma foobar (P1 P2 Q : uPred) :
+  (P1 <-> P2) -> (uPred_or P1 Q) <-> (uPred_or P2 Q).
+Proof.
+  rewrite uPred_or_eq. (* This fails. *)
+Admitted.
+
+End T4.
+
+
+Module DesignFlaw.
+
+Record foo A := Foo { foo_car : A }.
+Definition bar : foo _ := Foo nat 10.
+
+Definition app (f : foo nat -> nat) x := f x.
+
+Goal app (foo_car _) bar = 10.
+Proof.
+unfold app.  (* mkApp should produce a Proj *)
+Fail set x := (foo_car _ _).
+Admitted.
+
+End DesignFlaw.
+
+
+Module Bug.
+
+Record foo A := Foo { foo_car : A }.
+
+Definition bar : foo _ := Foo nat 10.
+
+Variable alias : forall A, foo A -> A.
+
+Parameter e : @foo_car = alias.
+
+Goal foo_car _ bar = alias _ bar.
+Proof.
+Fail rewrite e.  (* Issue: #86 *)
+Admitted.
+
+End Bug.
+
+
-- 
cgit v1.2.3