The Coq mailing list

[Stefan Karrmann <sk AT mathematik.uni-ulm.de>]

Dear Pierre,

Pierre Casteran (Thu, Jun 17, 2004 at 10:01:53AM +0200):
>   You can find in Coq's standard library the module
> 
> Coq.Wellfounded.Lexicographic_Product
> 
> which proves that the lexicogrqphic product of two wf sets
> is wf.

I tried (and succeeded, see below) this. The difficulty is to provide
the proof for (f:forall y:dom_ack,lex_ord_n2 y x->nat) after matching
the argument. It forces me to *proof* the definition of the argument
F in `Fix .. F ..'. Am I missing a simpler way? Something like:

Fixpoint ack2 (x:dom_ack) : nat :=
   match x with
      | existS 0 n
      => n+1
      | existS (S m) n
      => ack2 (existS B m (n+1))
      | existS (S m) (S n)
      => ack2 (existS B m (ack2 (existS B (S m) n)))
      end.

   with dom_ack as in the following code:

--- Begin ----------------------------------------------------------

Require Import Wf.
Require Import Relation_Operators.
Require Import Lexicographic_Product.

Definition A : Set := nat.
Definition B (_: A) := nat.
Definition ltA : A -> A -> Prop := lt.
Definition ltB  (x:A) : B x -> B x -> Prop := lt.

Definition lex_ord_n2 := (lexprod A B ltA ltB).

Definition dom_ack : Set := sigS B.
Definition dom_inj (m n:nat) : dom_ack := existS B m n.

Require Import Wf_nat.

Lemma wf_lt : well_founded lt.
Proof.
exact (well_founded_ltof nat (fun x : nat => x)).
Qed.

Lemma wf_ack : well_founded (A:=dom_ack) lex_ord_n2.
Proof.
exact (wf_lexprod A B ltA ltB wf_lt (fun x:A => wf_lt)).
Qed.

Lemma case2 : forall x y:A,lex_ord_n2 (dom_inj x y) (dom_inj x (S y)).
   Proof.
      intros.
      unfold dom_inj.
      unfold lex_ord_n2 in |- *.
      apply right_lex.
      unfold ltB in |- *.
      unfold lt in |- *.
      apply le_n.
   Qed.

Lemma case2_ : forall (x0:dom_ack) (x y:A),
   x0 = dom_inj x (S y) -> lex_ord_n2 (dom_inj x y) x0.
   Proof.
      intros x0 x y H.
      rewrite H.
      apply case2.
   Qed.

Lemma case1 : forall x y z:A,lex_ord_n2 (dom_inj x y) (dom_inj (S x) z).
   Proof.
      intros.
      unfold dom_inj.
      unfold lex_ord_n2 in |- *.
      apply left_lex.
      unfold ltA in |- *.
      clear y.
      clear z.
      unfold lt in |- *.
      apply le_n.
   Qed.

Lemma case1_ : forall (x0 : dom_ack) (z:A),projS1 x0 > 0 ->
               lex_ord_n2 (dom_inj (pred (projS1 x0)) z) x0.
   Proof.
      destruct x0 as (m, n).
      unfold projS1 in |- *.
      intros.
      set (y := pred m) in |- *.
      assert (m = S y).
       subst y.
         elim H.
        unfold pred in |- *.
          trivial.
        intros.
          unfold pred in |- *.
          trivial.
       assert (lex_ord_n2 (dom_inj y z) (dom_inj (S y) n)).
        apply case1.
        assert (dom_inj (S y) n = existS B m n).
         elim H0.
           unfold dom_inj in |- *.
           trivial.
         elim H2.
           apply H1.
   Qed.

Definition F (x:dom_ack) (f:forall y:dom_ack,lex_ord_n2 y x->nat) : nat.
   Proof.
      induction x as (m,n).
      induction m.
       intros.
         apply (S n).
       induction n.
        intros.
          set (y := existS B m 1) in |- *.
          assert (lex_ord_n2 y (existS B (S m) 0)).
         subst y.
           assert (lex_ord_n2 (dom_inj m 1) (dom_inj (S m) 0)).
          apply case1.
          assert (dom_inj m 1 = existS B m 1).
           unfold dom_inj in |- *.
             trivial.
           assert (dom_inj (S m) 0 = existS B (S m) 0).
            unfold dom_inj in |- *.
              trivial.
            elim H0.
              elim H1.
              apply H.
         apply (f y H).
        set (yi := existS B (S m) n) in |- *.
          assert (lex_ord_n2 yi (existS B (S m) (S n))).
         subst yi.
           assert (lex_ord_n2 (dom_inj (S m) n) (dom_inj (S m) (S n))).
          apply case2.
          assert (dom_inj (S m) n = existS B (S m) n).
           unfold dom_inj in |- *.
             trivial.
           assert (dom_inj (S m) (S n) = existS B (S m) (S n)).
            unfold dom_inj in |- *.
              trivial.
            elim H0.
              elim H1.
              apply H.
         intro.
           set (n2 := f yi H) in |- *.
           set (ya := existS B m n2) in |- *.
           assert (lex_ord_n2 ya (existS B (S m) (S n))).
          subst ya.
            assert (lex_ord_n2 (dom_inj m n2) (dom_inj (S m) (S n))).
           apply case1.
           assert (dom_inj m n2 = existS B m n2).
            unfold dom_inj in |- *.
              trivial.
            assert (dom_inj (S m) (S n) = existS B (S m) (S n)).
             unfold dom_inj in |- *.
               trivial.
             elim H1.
               elim H2.
               apply H0.
          apply (f ya H0).
   Qed.

Definition ack (m n : nat) : nat :=
   Fix wf_ack (fun _:dom_ack => nat) F (dom_inj m n).

Print ack.

---  End  ----------------------------------------------------------

> Stefan Karrmann wrote:
> >Pierre Casteran (Mon, Jun 14, 2004 at 07:45:06AM +0200):
> >
> >>Stefan Karrmann wrote:
> >>>How can I define recursive functions, e.g. the Ackermann function?
> >>>I found a definition which uses streams, but my try to define it
> >>>directly failed. Where can I find some hints? Is well-foundmess (Wf)
> >>>the right starting point?
> >>
> >>It  also possible to use a well founded order on pairs of natural 
> >>numbers (using Coq standard library) and define ackerman of type
> >>nat * nat -> nat (or Z * Z -> Z)
> >
> >
> >How can this be coded? The key relation is:
> >
> >Definition A : Set := pair nat nat.
> >Definition R (x:A)(y:A) : Prop := 
> >   ((fst x) < (fst y))
> >   \/ ((fst x = fst y)
> >      /\ (snd x < snd y) ).

-- 
Stefan Karrmann

The English have no respect for their language, and will not teach
their children to speak it.
                -- G. B. Shaw