The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

There is no way to ask for this sort of things in Coq v8.3. Simply put, the (internal) representation of proofs in progress does not allow to express that. After a serious re-engineering, Coq v8.4 has a command Grab Existential Variables, which brings every such hole as a goal. I also have a branch where refine directly exposes all the unsolved holes, but it still gives surprising (albeit correct) results when the hole is in a pattern-matching branch (if you want to play with it, you can find the branch on github: https://github.com/aspiwack/coq  (branch new-tacticals) ).

On 7 October 2012 03:00, S3 <scubed2 AT gmail.com> wrote:

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

>> To learn about accessibility and well-foundedness, I tried to prove that
>> the Ackermann function is well-founded. I'm using "Coq 8.3pl1 (July
>> 2011)".  (Yes, I know that I can just write it using 2 fixes.)
>>
>> I wrote the program at the bottom of this message. However, when I go to
>> prove the ack_step function (in the comment at the bottom), I leave 2
>> holes. However, refine only adds the 2nd as an obligation, skipping the
>> first.  How do I manually add an Existential as an Obligation? I tried
>> many variations of Focus Existential 1. Focus ?45. etc. but none of them
>> allow me to go to it. Why is it skipped? How do I Focus on it?
>>
>> (* Ackermann function.
>>
>> Attempt showing well-foundedness with the Ackermann function, even though
>> nest recursion handles it directly.
>>
>> I am having a problem with refine skipping a hole. How do I go to the
>> hole explicitly? *)
>>
>> Definition ack_ord (p q : nat*nat) := let (a1, b1) := p in let (a2, b2)
>> := q in a1 < a2 \/ (a1 = a2 /\ b1 < b2) .
>>
>> Theorem le_Sn_0 n: S n <= 0 -> False. intros. inversion H. Qed.
>>
>> Theorem le_S_both a b: a <= b -> S a <= S b. intros. induction H. apply
>> le_n.
>>
>> apply le_S. apply IHle. Qed.
>>
>> Theorem le_0 a: 0 <= a. induction a. apply le_n.
>>
>> apply le_S. apply IHa. Qed.
>>
>> Theorem ack_wf_b: forall a, Acc ack_ord (a, 0) -> forall b, Acc ack_ord
>> (a, b). intros. induction b. apply H.
>>
>> apply Acc_intro. induction y. intros. induction H0. apply (Acc_inv IHb).
>> apply or_introl. apply H0.
>>
>> induction H0. rewrite H0. clear H0 a0. inversion H1. apply IHb.
>>
>> apply IHb. apply or_intror. apply conj. apply eq_refl.
>>
>> apply H2. Qed.
>>
>> Theorem ack_wf: well_founded ack_ord. unfold well_founded. induction a.
>> apply ack_wf_b. clear b. induction a. apply Acc_intro. induction y.
>> intros. induction H. apply le_Sn_0 in H. apply (False_ind _ H).
>>
>> induction H. apply le_Sn_0 in H0. apply (False_ind _ H0).
>>
>> apply Acc_intro. induction y. intros. apply ack_wf_b. induction H.
>> inversion H. apply IHa.
>>
>> apply (Acc_inv IHa). apply or_introl. apply H1.
>>
>> induction H. apply le_Sn_0 in H0. apply (False_ind _ H0). Qed.
>>
>> (* Theorem ack_step x (f : forall y, ack_ord y x -> nat) : nat. refine (
>> match x as z return x = z -> nat with | pair a b => fun H => match a as c
>> return a = c -> nat with | 0 => fun _ => S b | S a0 => fun H2 => f ( a0,
>> match b as d return b = d -> nat with | 0 => fun _ => 1 | S b0 => fun H3
>> => f (a, b0) _ end (eq_refl b) ) _ end (eq_refl a) end (eq_refl x) ).
>>
>> (* Skips first hole for f (a, b0) _ *)
>>
>> (* 2nd hole *)
>>
>> rewrite H. rewrite H2. apply or_introl. apply le_n.
>>
>> (* Can't save, how do I go back to first Existential hole? *)
>>
>> No more subgoals but non-instantiated existential variables: Existential
>> 1 = ?56 : [x : nat * nat f : forall y : nat * nat, ack_ord y x -> nat a :
>> nat b : nat a0 := a : nat b0 := b : nat H : x = (a, b) a1 : nat a2 := a1
>> : nat H2 : a0 = S a1 b1 : nat b2 := b1 : nat H3 : b0 = S b1 |- ack_ord
>> (a0, b2) x]
>>
>> *)

> I am not sure if the following solution is an acceptable answer. In
> general, you can use the "instantiate" tactic to fill an existential. But
> in doing so, you have to provide a full term.
>
> =======================
>

> Theorem ack_step x (f : forall y, ack_ord y x -> nat) : nat. refine ( match
> x as z return x = z -> nat with | pair a b => fun H => match a as c return

> a = c -> nat with | 0 => fun _ => S b | S a0 => fun H2 => let g := fun b0
> H3 => _ in f ( a0, match b as d return b = d -> nat with | 0 => fun _ => 1
> | S b0 => fun H3 => f (a, b0) (g b0 H3) end (eq_refl b) ) _ end (eq_refl

> a) end (eq_refl x) ).
>

> (* Skips first hole for f (a, b0) _ *) subst. right; repeat constructor.

>
> (* 2nd hole *)
>
> subst. apply or_introl. apply le_n.

Yes, I saw in the documentation about giving explicit
terms for Existentials.  I wanted to use the interactive
theorem prover to fill in the gaps.

The trick of using a separate function and allowing
me to fill it in that way works.  Thanks!

I'm still a bit curious if there's a way to tell
it that I want to interactively edit the hole.
But, my immediate problem is solved with that workaround.

- --
$_="sccc,gB1,a_oo,JosBackuSa,g11,ug1a,oscc,cBBg,JcgaBuucaB_s11_Juc_c";
while(($c,$b,$a)=m/^(.)([^,]*),(.*)$/){$_=$a;s/$c/$b/g;}
print map chr length,split /_/;
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v2.0.17 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/

iEYEARECAAYFAlBw1DQACgkQxzVgPqtIcfs5hACeJnlUjQ/6mk6K+MV/SFAWHilC
C30An3ntHP3go62WUfYPfRReOKNf14UE
=15cm
-----END PGP SIGNATURE-----