Question About Assignment12_06

[amityaffliction]

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

[jaewooklee93]

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.

[amityaffliction]

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

[jaewooklee93]

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.

[amityaffliction]

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

[amityaffliction]

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?

[jaewooklee93]

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.

[amityaffliction]

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

[rhs0266]

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 @_@

[jaewooklee93]

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).