Open amityaffliction opened 9 years ago
Well.. In the case of my solution, I didn't use any of progress
, stuck
, preservation
concept, but I used one remember
and very delicate assert
twice.
Thank you for answering! could you give me little more informal intuition on the property that you asserted? I'm really stuck and can't make progress
Actually, informal idea of proof is devastingly trivial. The problem is how to represent that idea in Coq formally.
[Informal Proof]
Let p = tapp tloop (tnat 0)
, there exist q, r
such that p ==> q ==> r ==> p
.
Thus, p ==>* t
implies t = p or q or r
. Therefore, t
is not a normal form.
Oh!! so (tapp tloop (tnat 0)) has only few forms before getting back to original one and proving by existential quantification. I carelessly thought there would be so many of internal forms. proving this way is so clever! thank you
When proving p ==>* t implies t = p or q or r. trouble arise when p==>t is in context. it's easy to show "p multi steps to some t" but when it is in the context, it seems unsolvable either by inversion or induction. for example, when H: p ==> * t, inversion/induction on H or t won't get any useful things.. I wonder if there is some tactics for coq to infer something from p ==> t .. and is this provable without some deterministic property lemma?
Yes, it is related to the deterministic
property, or more precisely, the uniqueness of q
and r
. (If q
is not unique, p ==> t
doesn't implies t = q
.) But I didn't directly prove or use the general deterministic
Lemma itself. (It is truly overkill.) I only proved determinism for p,q,r
using assert
.
Well.. I agree that this problem is really difficult. As I mentioned above, the real problem is how to represent such informal idea in Coq.
After proving determinism, I tried to prove "p ==>* t implies t = p or q or r" part, but cant figure out what tactic should be used. inversion on p==>*t and following hypothesis will unfold infinitely and not exactly sure it is solvable with induction. I keep get not powerful Inductive Hypothesis. I think keep inversion on H and at some point, I should be able to prove within context that it circulates. but it seems it's not reachable with inversion or induction... is it related with remember tactic?? asdlkfjasdlkfasdf T_T
I also found p, q, r. But how can prove t=p or q or r
? I am trying to proof with assert (t=p or t=q or t=z)
, but it is quite difficult assertion... Fall into the infinite circulation @_@
Yes.. I've also tried it with simple induction
, but never succeeded.
With remember
, you can define your own predicate like this.
remember (fun n => exists k, n = 5 * k + 1) as P.
And then you can use your predicate as invariant.
assert (forall n m, m = n + 5 -> P n -> P m).
I know tloop is infinite so resulting x from tloop will also take step
I tried to prove directly but failed and tried to solve some properties with progress, stuck, preservation
after digging I got into this state. with these properties I tried to prove it
but keep stuck when (value x) in the context. will there be better approach then this??
or am I missing some lemma to assert to get to the goal?
x : tm A : tapp tloop (tnat 0) ==>* x B : ~ (exists t' : tm, x ==> t') C : \empty |- tapp tloop (tnat 0) \in TNat D : \empty |- x \in TNat E : value x \/ (exists t' : tm, x ==> t') F : normal_form step x /\ ~ value x -> False (that is, x is not stuck) __(1/1) False