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]

*)

- -- 
$_="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/

iEYEARECAAYFAlBwdaUACgkQxzVgPqtIcfuU9ACfZK3zfxqINhYXXcpIGPelB/ML
FYYAnA4G/uNtHc9ihScfvAP1g569iEAW
=M++a
-----END PGP SIGNATURE-----