diff options
Diffstat (limited to 'test-suite/bugs/closed/3531.v')
-rw-r--r-- | test-suite/bugs/closed/3531.v | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3531.v b/test-suite/bugs/closed/3531.v new file mode 100644 index 00000000..fd080a6b --- /dev/null +++ b/test-suite/bugs/closed/3531.v @@ -0,0 +1,53 @@ +(* File reduced by coq-bug-finder from original input, then from 270 lines to +198 lines, then from 178 lines to 82 lines, then from 88 lines to 59 lines *) +(* coqc version trunk (August 2014) compiled on Aug 19 2014 14:40:15 with OCaml +4.01.0 + coqtop version cagnode17:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk +(56ece74efc25af1b0e09265f3c7fcf74323abcaf) *) +Require Import Coq.Lists.List. +Set Implicit Arguments. +Definition mem := nat -> option nat. +Definition pred := mem -> Prop. +Delimit Scope pred_scope with pred. +Definition exis A (p : A -> pred) : pred := fun m => exists x, p x m. +Notation "'exists' x .. y , p" := (exis (fun x => .. (exis (fun y => p)) ..)) : +pred_scope. +Definition emp : pred := fun m => forall a, m a = None. +Definition lift_empty (P : Prop) : pred := fun m => P /\ forall a, m a = None. +Notation "[[ P ]]" := (lift_empty P) : pred_scope. +Definition pimpl (p q : pred) := forall m, p m -> q m. +Notation "p ==> q" := (pimpl p%pred q%pred) (right associativity, at level 90). +Definition piff (p q : pred) : Prop := (p ==> q) /\ (q ==> p). +Notation "p <==> q" := (piff p%pred q%pred) (at level 90). +Parameter sep_star : pred -> pred -> pred. +Infix "*" := sep_star : pred_scope. +Definition memis (m : mem) : pred := eq m. +Definition mptsto (m : mem) (a : nat) (v : nat) := m a = Some v. +Notation "m @ a |-> v" := (mptsto m a v) (a at level 34, at level 35). +Lemma piff_trans: forall a b c, (a <==> b) -> (b <==> c) -> (a <==> c). +Admitted. +Lemma piff_refl: forall a, (a <==> a). +Admitted. +Definition stars (ps : list pred) := fold_left sep_star ps emp. +Lemma flatten_exists: forall T PT p ps P, + (forall (a:T), (p a <==> exists (x:PT), stars (ps a x) * [[P a x]])) + -> (exists (a:T), p a) <==> + (exists (x:(T*PT)), stars (ps (fst x) (snd x)) * [[P (fst x) (snd x)]]). +Admitted. +Goal forall b, (exists e1 e2 e3, + (exists (m : mem) (v : nat) (F : pred), b) + <==> (exists x : e1, stars (e2 x) * [[e3 x]])). + intros. + Set Printing Universes. + Show Universes. + do 3 eapply ex_intro. + eapply piff_trans; [ apply flatten_exists | apply piff_refl ]; intros. + eapply piff_trans; [ apply flatten_exists | apply piff_refl ]; intros. + eapply piff_trans; [ apply flatten_exists | apply piff_refl ]; intros. + assert (H : False) by (clear; admit); destruct H. + Grab Existential Variables. + admit. + admit. + admit. + Show Universes. +Time Qed.
\ No newline at end of file |