The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Sat, 06 Oct 2012 11:17:09 -0700,
S3 
<scubed2 AT gmail.com>
 a écrit :

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

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.