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
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
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}".
*)
|
