diff options
Diffstat (limited to 'test-suite/bugs/closed/3732.v')
| -rw-r--r-- | test-suite/bugs/closed/3732.v | 105 |
1 files changed, 105 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3732.v b/test-suite/bugs/closed/3732.v new file mode 100644 index 00000000..76beedf6 --- /dev/null +++ b/test-suite/bugs/closed/3732.v @@ -0,0 +1,105 @@ +Require Import TestSuite.admit. +(* File reduced by coq-bug-finder from original input, then from 2073 lines to 358 lines, then from 359 lines to 218 lines, then from 107 lines to 92 lines *) +(* coqc version trunk (October 2014) compiled on Oct 11 2014 1:13:41 with OCaml 4.01.0 + coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (d65496f09c4b68fa318783e53f9cd6d5c18e1eb7) *) +Require Coq.Lists.List. + +Import Coq.Lists.List. + +Set Implicit Arguments. +Global Set Asymmetric Patterns. + +Section machine. + Variables pc state : Type. + + Inductive propX (i := pc) (j := state) : list Type -> Type := + | Inj : forall G, Prop -> propX G + | ExistsX : forall G A, propX (A :: G) -> propX G. + + Implicit Arguments Inj [G]. + + Definition PropX := propX nil. + Fixpoint last (G : list Type) : Type. + exact (match G with + | nil => unit + | T :: nil => T + | _ :: G' => last G' + end). + Defined. + Fixpoint eatLast (G : list Type) : list Type. + exact (match G with + | nil => nil + | _ :: nil => nil + | x :: G' => x :: eatLast G' + end). + Defined. + + Fixpoint subst G (p : propX G) : (last G -> PropX) -> propX (eatLast G) := + match p with + | Inj _ P => fun _ => Inj P + | ExistsX G A p1 => fun p' => + match G return propX (A :: G) -> propX (eatLast (A :: G)) -> propX (eatLast G) with + | nil => fun p1 _ => ExistsX p1 + | _ :: _ => fun _ rc => ExistsX rc + end p1 (subst p1 (match G return (last G -> PropX) -> last (A :: G) -> PropX with + | nil => fun _ _ => Inj True + | _ => fun p' => p' + end p')) + end. + + Definition spec := state -> PropX. + Definition codeSpec := pc -> option spec. + + Inductive valid (specs : codeSpec) (G : list PropX) : PropX -> Prop := Env : forall P, In P G -> valid specs G P. + Definition interp specs := valid specs nil. +End machine. +Notation "'ExX' : A , P" := (ExistsX (A := A) P) (at level 89) : PropX_scope. +Bind Scope PropX_scope with PropX propX. +Variables pc state : Type. + +Inductive subs : list Type -> Type := +| SNil : subs nil +| SCons : forall T Ts, (last (T :: Ts) -> PropX pc state) -> subs (eatLast (T :: Ts)) -> subs (T :: Ts). + +Fixpoint SPush G T (s : subs G) (f : T -> PropX pc state) : subs (T :: G) := + match s in subs G return subs (T :: G) with + | SNil => SCons _ nil f SNil + | SCons T' Ts f' s' => SCons T (T' :: Ts) f' (SPush s' f) + end. + +Fixpoint Substs G (s : subs G) : propX pc state G -> PropX pc state := + match s in subs G return propX pc state G -> PropX pc state with + | SNil => fun p => p + | SCons _ _ f s' => fun p => Substs s' (subst p f) + end. +Variable specs : codeSpec pc state. + +Lemma simplify_fwd_ExistsX : forall G A s (p : propX pc state (A :: G)), + interp specs (Substs s (ExX : A, p)) + -> exists a, interp specs (Substs (SPush s a) p). +admit. +Defined. + +Goal forall (G : list Type) (A : Type) (p : propX pc state (@cons Type A G)) + (s : subs G) + (_ : @interp pc state specs (@Substs G s (@ExistsX pc state G A p))) + (P : forall _ : subs (@cons Type A G), Prop) + (_ : forall (s0 : subs (@cons Type A G)) + (_ : @interp pc state specs (@Substs (@cons Type A G) s0 p)), + P s0), + @ex (forall _ : A, PropX pc state) + (fun a : forall _ : A, PropX pc state => P (@SPush G A s a)). + intros ? ? ? ? H ? H'. + apply simplify_fwd_ExistsX in H. + firstorder. +Qed. + (* Toplevel input, characters 15-19: +Error: Illegal application: +The term "cons" of type "forall A : Type, A -> list A -> list A" +cannot be applied to the terms + "Type" : "Type" + "T" : "Type" + "G0" : "list Type" +The 2nd term has type "Type@{Top.53}" which should be coercible to + "Type@{Top.12}". + *)
\ No newline at end of file |