The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

Le Thu, 16 Jun 2011 11:20:51 -0500,
Paul Tarau 
<paul.tarau AT gmail.com>
 a écrit :

> My next challenge is to describe arithmetic computations directly on
> binary trees - a kind of hereditary base 2 exponent notation - as used
> in Goodstein's theorem). It is interesting because it allows computing
> with gigantic numbers that binary representations cannot handle. The
> intuition is that the first argument of the constructor C represents
> an exponent of 2, recursively

And as well binary representation allow computing with other numbers
that your representation cannot!

> Unfortunately, Coq rejects this with:
> 
> Error: Cannot guess decreasing argument of fix.
> 
> I think that termination of the mutually recursive Fixpoint
> follows from the fact that at each step in every match
> in every definition at least one argument becomes structurally
> simpler - so every reduction in the mutually recursive
> definition makes progress towards termination.

It is the fact in coq, but not in your example.

> Is it the mutual recursion that confuses Coq? Doest it make sense to
> use the bijection to nat "t2n" as a measure? Defining a well founded
> relation seems tricky as one needs successor/predecessor to work
> first.

It is tricky, but not impossible (I did it).
I send what I did; do not expect it to be easy to read.

I never use Program or Function; because it is not so often I would
have use of it, there are some limitations, and I don't understand all
what is performed (not because it is too complex, but because I have
always been too lazy to try to use it). But I guess, that your example
is a typical case where you may wish to use it.

I also put a function to convert [nat] to [T], but I guess it can be
simplified (by removing some of its specifications).

I changed the definition of "exp2", so that all multiplications were
removed.

> P.S. The Haskell equivalent works as expected so it is unlikely that I
> have any logical erros in my definition. Here it is:
> 
> data T = E|C T T deriving (Eq,Read,Show)
> 
> s0 E = E
> s0 (C E y) = C (s0 (s0 y)) (s1 (s0 y))
> s0 (C (C _ _) _) = E
> 
> s1 E = E
> s1 (C E y) = s1 y
> s1 (C (C a b) y) = C (p2 a b) y
> 
> p2 E E = E
> p2 E (C a b) = C (C (s0 a) (s1 a)) b
> p2 (C a b) y = C E (p2 (p2 a b) y)
> 
> -- successor and predecessor on type T
> s x = C (s0 x) (s1 x)
> p (C x y) = p2 x y
> 
> -- nat to T conversion
> n2t 0 = E
> n2t x | x>0 = s (n2t (x-1))
> 
> -- T to nat conversion
> t2n E = 0
> t2n (C x y) = 2^(t2n x)*(2*(t2n y)+1)
> 
> -- tests
> check = map (t2n.n2t) [0..31]
> pcheck = map (t2n.p.s.n2t) [0..31]

In fact, assuming coq is consistant, your function is good and
terminates.
(* This has turned now into a fairly complete implementation of
bijective base-2 arithmetic, combined with a bijective Goedel
numbering scheme for sets and lists - using exclusively structural
induction:

http://logic.csci.unt.edu/tarau/research/2011/Bij2.v.txt.

Comments on the code are welcome - I am and I will be forever a beginner :-)

My next challenge is to describe arithmetic computations directly on
binary trees - a kind of hereditary base 2 exponent notation - as used
in Goodstein's theorem). It is interesting because it allows computing
with gigantic numbers that binary representations cannot handle. The
intuition is that the first argument of the constructor C represents
an exponent of 2, recursively
*)

Inductive T : Set :=
| E : T
| C : T -> T -> T.

Delimit Scope T_scope with T.
Bind Scope T_scope with T.
Arguments Scope T [T_scope].

Require Import Plus.
Require Import Le.

Fixpoint exp2 (x y : nat) : nat :=
match x with
| 0 => y
| S n => (exp2 n y)+(exp2 n y)
end.

Definition pdouble (x : nat) : nat := S (x + x).

(* a bijection from T to nat *)
Fixpoint t2n (t : T) {struct t} : nat :=
match t with
| E => 0
| C x y => exp2 (t2n x) (pdouble (t2n y))
end.

Eval compute in t2n (C (C E E) (C E E)).

(* Converting [T] to [nat];
   note that:
   - we use "specified" functions; we were not forced to do so,
     we could have specified it with lemmas
   - we didn't use Program nor Function, but they could have been usefull
   - we do not require it to compute successor or predecessor, so this
     part can be removed if we don't want to convert [T] to [nat]
*)

Ltac nat_simpl_aux :=
  rewrite <- plus_n_O in *
||rewrite <- plus_n_Sm in *.

Ltac nat_simpl := repeat nat_simpl_aux.

Fixpoint div2 (n : nat) : {c : nat & {n = c+c}+{n = S (c+c)}}.
refine (match n with
        | O => existT _ O (left _ _)
        | S n => let (c, even) := div2 n in
                 if even
                 then existT _ c (right _ _)
                 else existT _ (S c) (left _ _)
        end);
(clear -_H||clear); abstract (nat_simpl; subst; easy).
Defined.

Definition wfdiv2: forall n, Acc (fun x y => y = x+x) (S n).
refine (fun n =>
     (fix wfdiv2 (n0 n1 n2 : nat) {struct n0}:
      n0 = n2 + n1 -> Acc (fun x y : nat => y = x + x) (S n1) :=
      match n0 as n3 return n3 = _ -> _ with
      | 0 => fun _ => Acc_intro (S n1) _
      | S n0 =>
          fun _ =>
            Acc_intro (S n1)
              (fun y =>
                match y as y0 return S n1 = y0+y0 -> Acc _ y0 with
                | O => _
                | S y => fun _ => wfdiv2 n0 y (n2+y) _
                end)
      end) n n 0 (eq_refl n)).
Proof.
clear - _H.
abstract (
  intros; exfalso; destruct n1;
  [destruct y; simpl in H; inversion H;
   destruct y; simpl in _H; discriminate
  |nat_simpl; discriminate]
).
Proof.
simpl; clear.
abstract (intros; exfalso; discriminate).
Proof.
simpl in *; clear - _H _H0.
abstract (
 revert _H; inversion _H0; clear;
 nat_simpl;
 rewrite plus_assoc;
 intro H0; inversion H0;
 split).
Defined.

Definition nsplit (n : nat)
: (n = O) + {c : nat * nat | n = exp2 (fst c) (pdouble (snd c))}.
refine (match n as n0 return (n0 = _)+{_ | n0 = _} with
        | 0 => inl _ _
        | S n0 =>
            inr _
              ((fix nsplit n1 (H: Acc _ n1) {struct H}
                : {c | n1 = exp2 (fst c) (pdouble (snd c))} :=
                match H with
                | Acc_intro H0 =>
                    let (x, s0) := div2 n1 in
                    match s0 with
                    | left e => let (pair, _) := nsplit _ (H0 _ e) in
                                exist _ (S (fst pair), snd pair) _
                    | right e => exist _ (0, x) e
                    end
                end) (S n0) (wfdiv2 n0))
        end).
Proof.
 clear; split.
Proof.
 clear - e _H; simpl.
 abstract (now subst).
Defined.

Lemma exp_pos: forall a b, exp2 a (S b) = S (pred (exp2 a (S b))).
Proof.
 intros a b; induction a; simpl.
  split.
 now destruct (exp2 a (S b)); simpl in *.
Qed.

Definition wfsplit1 (n y k x n1 : nat)
 : S n = n1 + k -> k = exp2 x (pdouble y) -> {n2 : nat | n = n2 + y}.
refine (fun _ _ =>
       (fix wfsplit1 (x n1 : nat) :=
        match x as x0 return S n = n1 + exp2 x0 (pdouble y) -> _ with
        | O => fun _ => exist _ (n1+y) _
        | S x =>  fun _ => wfsplit1 x (n1 + exp2 x (pdouble y)) _
        end) x n1 _).
Proof.
 simpl in *; clear - _H1.
 abstract (unfold pdouble in _H1; nat_simpl; rewrite <- plus_assoc;
           now inversion_clear _H1).
Proof.
 simpl in *; clear - _H1.
 abstract (now rewrite <- plus_assoc).
Proof.
 abstract (now subst).
Defined.

Definition wfsplit2 (x k y n n1 : nat)
 : S n = n1 + k -> k = exp2 y (pdouble x) -> {n2 | n = n2 + y}.
refine (fun _ _ =>
       (fix wfsplit2 (y n n1 : nat)
        : S n = n1 + exp2 y (pdouble x) -> {n2 | n = n2 + y} :=
        match y as y0 return _ = _ + exp2 y0 _ -> {_ | _ = _ + y0} with
        | O => fun _ => exist _ n _
        | S y => match n as n0 return S n0 = _ -> {_ | n0 = _} with
                 | O => fun _ => _
                 | S n =>
                     fun _ =>
                       let (n2, _) :=
                         wfsplit2 y n (n1+pred (exp2 y (pdouble x))) _
                       in exist _ n2 _
                 end
        end) y n n1 _).
Proof.
 clear; abstract (now nat_simpl).
Proof.
 clear - _H1; simpl in *.
 abstract (exfalso; unfold pdouble in _H1;
           rewrite exp_pos in _H1;
           clear - _H1; nat_simpl;
           destruct n2; simpl in _H1; discriminate).
Proof.
 clear - _H1.
 abstract (simpl in *; unfold pdouble in *;
           rewrite exp_pos in *;
           simpl in *; clear - _H1; nat_simpl;
           rewrite <- plus_assoc; inversion _H1; split).
Proof.
 clear - _H2.
 abstract (nat_simpl; inversion _H2; split).
Proof.
 abstract (now subst).
Defined.

Inductive even_odd_decomp (x y : nat) : Prop :=
| Even_decomp: forall c, y = exp2 x (pdouble c) -> even_odd_decomp x y
| Odd_decomp: forall c, y = exp2 c (pdouble x) -> even_odd_decomp x y
.

Definition wfsplit : forall n, Acc even_odd_decomp n.
Proof.
 intros n.
 generalize (eq_refl _: n = 0+n).
 generalize 0 at 1.
 generalize n at 2 3.
 induction n; intros.
  split; intros.
abstract (
  exfalso;
  destruct n;
  [destruct H0; unfold pdouble in H0;
   [rewrite exp_pos in H0; discriminate
   |rewrite exp_pos in H0; discriminate]
  |nat_simpl; discriminate]).
 split; intros.
 destruct H0.
  destruct (wfsplit2 _ _ _ _ _ H H0).
  exact (IHn _ _ e).
 destruct (wfsplit1 _ _ _ _ _ H H0).
 exact (IHn _ _ e).
Defined.

Print wfsplit.

Definition n2t (n : nat) : {t : T | n = t2n t}.
refine ((fix n2t n (H: Acc _ n) : {t : T | n = t2n t} :=
         match H with
         | Acc_intro H0 =>
             match nsplit n with
             | inl _ => existT _ E _
             | inr p =>
                 let (pair, H) := p in
                 let (exp, _) := n2t (fst pair)
                                     (H0 _ (Even_decomp _ _ (snd pair) H))
                 in
                 let (rem, _) := n2t (snd pair)
                                     (H0 _ (Odd_decomp _ _ (fst pair) H))
                 in
                 existT _ (C exp rem) _
             end
         end) n (wfsplit n)).
Proof.
 clear - e; simpl; assumption.
Proof.
 clear - _H _H0 H1; simpl.
 abstract (rewrite <- _H; rewrite <- _H0; assumption).
Defined.

Definition n2t' n := let (t, _) := n2t n in t.

Eval compute in (n2t' 467).

Recursive Extraction n2t'.

(* Here begins the effective part for computing successor and predecessor *)

(* [sRel a b] means that [b] is the successor of [a] *)
Inductive sRel: T -> T -> Prop :=
| sRel0: sRel E (C E E)
| sRel1: forall a2 sa21 sa22,
         sRel a2 (C sa21 sa22) ->
         forall ssa21,
         sRel sa21 ssa21 ->
         sRel (C E a2) (C ssa21 sa22)
| sRel2: forall pa1 a1,
         sRel pa1 a1 ->
         forall a2,
         sRel (C a1 a2) (C E (C pa1 a2)).

Lemma sRel_spe: forall a b, sRel a b -> S (t2n a) = t2n b.
Proof.
 intros a b H; induction H; simpl in *.
   split.
  clear H H0; nat_simpl.
  rewrite <- IHsRel2; clear IHsRel2 ssa21.
  simpl; nat_simpl.
  rewrite <- IHsRel1; clear.
  nat_simpl; split.
 clear H; rewrite <- IHsRel; clear.
 simpl; nat_simpl; split.
Qed.

(* The well formed induction we need to build our recursive functions;
   it is hard to guess it at first sight;
   the way I got them, was by defining first the recursive functions
   and then to see what were the required constraints to make it work.
*)
Inductive SRel: T -> T -> Prop :=
| SRel0: forall a b, SRel a (C a b)
| SRel1: forall a, SRel a (C E a)
| SRel2: forall a b c, sRel a (C b c) -> SRel b (C E a)
| SRel3: forall a b, SRel a (C E (C a b))
| SRel4: forall a b c, sRel a b -> SRel (C a c) (C b c).

Ltac le_simpl := (repeat apply le_n_S); apply le_0_n||apply le_n||idtac.

(* To show that this predicate defines a well founded relation,
   we will need some strong induction,
   given by [SRel_spe], for that we need some intermediate lemma *)
Lemma SRel_spe_aux: forall a b, S a <= exp2 a (S b).
Proof.
 intros; induction a; simpl; le_simpl.
 apply le_trans with (S (exp2 a (S b))); le_simpl.
  assumption.
 apply (plus_le_compat_r 1 _ (exp2 a (S b))).
 rewrite exp_pos; le_simpl.
Qed.

Lemma SRel_spe: forall a b, SRel a b -> S (t2n a) <= t2n b.
Proof.
 intros a b H; induction H; simpl; unfold pdouble.
     apply SRel_spe_aux.
    le_simpl; apply le_plus_trans; le_simpl.
   rewrite <- plus_Sn_m.
   apply le_plus_trans.
   rewrite (sRel_spe _ _ H); simpl; clear.
   unfold pdouble; apply SRel_spe_aux.
  rewrite plus_n_Sm.
  apply le_plus_trans.
 apply SRel_spe_aux.
 generalize (t2n c + t2n c).
 intros; rewrite <- (sRel_spe _ _ H); clear.
 simpl.
 apply (plus_le_compat_r 1 _ (exp2 (t2n a) (S n))).
 rewrite exp_pos; le_simpl.
Qed.

(* now the well foundness of our relation *)
Fixpoint SRel_wf_aux (n : nat) (t : T) : S (t2n t) <= n -> Acc SRel t.
refine (match n as n0 return _ <= n0 -> _ with
        | O => _
        | S n => fun _ => Acc_intro _ (fun y Hy => SRel_wf_aux n y _)
        end).
Proof.
 clear.
 abstract (intros; exfalso; inversion H).
Proof.
 clear - Hy _H.
 abstract exact (le_trans _ _ _ (SRel_spe _ _ Hy) (le_S_n _ _ _H)).
Defined.

(* mutually recursive components of s,p *)
Fixpoint s (a: T) (H: Acc SRel a) {struct H}: {b: T | sRel a b}
with     p (a: T) (H: Acc SRel a) {struct H}: (a=E)+{b: T | sRel b a}.
refine (match H with
        | Acc_intro H =>
          let S := fun x Hx => s x (H _ Hx) in
          let P := fun x Hx => p x (H _ Hx) in
          (match a as a0 return _ -> (forall c, _ -> {b|_}) -> {_|sRel a0 _} with
          | E => fun _ _ => exist _ (C E E) _
          | C a1 a2 =>
              fun P S =>
              match P a1 _ with
              | inl _ => let (x, H') := S a2 _ in
                         match x as x0 return _ -> _ with
                         | E => _
                         | C x1 x2 =>
                           fun _ =>
                           let (x, _) := S x1 _ in
                           exist _ (C x x2) _
                         end H'
              | inr (exist x _) => exist _ (C E (C x a2)) _
              end
          end) P S
        end).
Proof.
 constructor.
Proof.
 constructor.
Proof.
 clear - y; abstract (subst; constructor).
Proof.
 clear.
 abstract (intros; exfalso; inversion H).
Proof.
 clear - y _H H'.
 abstract (subst; econstructor; eassumption).
Proof.
 clear - y _H _H0.
 abstract (subst; econstructor; eassumption).
Proof.
 now constructor.
(**)
refine (match H with
        | Acc_intro H =>
          let S := fun x Hx => s x (H _ Hx) in
          let P := fun x Hx => p x (H _ Hx) in
          (match a as a0
           return _ -> (forall b, SRel _ a0 -> _) -> (a0=_)+{_|sRel _ a0} with
          | E => fun _ _ => inl _ _
          | C a1 a2 =>
              fun P S =>
              inr _
              match P a1 _ with
              | inl _ =>
                (match a2 as a0
                 return (forall b, SRel _ (C _ a0) -> {c|_}) ->
                        {_|sRel _ (C _ a0)}
                 with
                | E => fun _ => exist _ E _
                | C x1 x2 => fun S =>
                             let (x, _) := S x1 _ in
                             exist _ (C x x2) _
                end)
                S
              | inr (exist x _) =>
                match P (C x a2) _ with
                | inl _ => _
                | inr (exist x0 _) => exist _ (C E x0) _
                end
              end
          end)
          P S
        end).
Proof.
 split.
Proof.
 constructor.
Proof.
 clear - y; abstract (subst; constructor).
Proof.
 clear - y; abstract (subst; constructor).
Proof.
 clear - y _H; abstract (subst; constructor; assumption).
Proof.
 clear - y0; abstract (constructor; assumption).
Proof.
 clear - y1; abstract (exfalso; inversion y1).
Proof.
 econstructor; eassumption.
Defined.

(* mutually recursive components of s,p *)
Definition s_ (a:T) :=
 let (r, _) := s a (SRel_wf_aux (S (t2n a)) a (le_n _)) in r.
Definition p_ (a:T) :=
 match p a (SRel_wf_aux (S (t2n a)) a (le_n _)) with
 | inl _ => None
 | inr (exist x _) => Some x
 end.
Definition p__ (a:T) :=
 match p_ a with
 | None => E
 | Some x => x
 end.

Lemma s_spe: forall t, t2n (s_ t) = S (t2n t).
Proof.
 unfold s_; intros.
 symmetry.
 apply sRel_spe.
 generalize (SRel_wf_aux (S (t2n t)) t (le_n (S (t2n t)))).
 intros.
 now destruct (s t a).
Qed.

Lemma p_spe: forall t, t=E \/ S (t2n (p__ t)) = t2n t.
Proof.
 unfold p__, p_; intros.
 generalize (SRel_wf_aux (S (t2n t)) t (le_n (S (t2n t)))).
 intros.
 destruct (p t a).
  now left.
 right.
 destruct s0.
 now apply sRel_spe.
Qed.

Example E1 := Eval compute in (n2t' 136).
Example E2 := Eval compute in (s_ E1).
Example RES := Eval compute in ((E1, t2n E1), (E2, t2n E2)).
Print RES.

Extraction s.