The Coq mailing list

[S3 <scubed2 AT gmail.com>]

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