The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi, 

> I was experimenting with reproving the Peano induction principle for binary 
> positive integers, and got this accepted:
> 
> Require Import BinPos.
> 
> Open Scope positive_scope.
> 
> Lemma Pind2: forall P:positive->Prop,
>   P 1 -> (forall p:positive, P p -> P (Psucc p)) ->
>   forall p:positive, P p.
> Proof.
> fix 4.
> intros P H1 Hind.
> assert (forall p:positive, P (p ~ 0)).
> induction p using Pind2.
> apply Hind in H1.
> simpl in H1.
> assumption.
> apply Hind in IHp.
> simpl in IHp.
> apply Hind in IHp.
> simpl in IHp.
> assumption.
> 
> destruct p.
> pose proof (H p).
> apply Hind in H0.
> simpl in H0.
> assumption.
> apply H.
> assumption.
> Qed.
> 
> I was trying to analyze why the guardedness checker accepted this proof, 
> but 
> the generated proof term is weird:
> 
> Pind2 = 
> fix Pind2 (P : positive -> Prop) (H1 : P 1)
>           (Hind : forall p : positive, P p -> P (Psucc p))
>           H:=
>            fun p : positive =>
>            Pind2 (fun p0 : positive => P p0~0) (let H2 := Hind 1 H1 in H2)
>              (fun (p0 : positive) (IHp : P p0~0) =>
>               let IHp0 := Hind p0~0 IHp in let IHp1 := Hind p0~1 IHp0 in 
> IHp1)
>              p (p : positive) {struct H} : H1 p :=
>   match p as p0 return (P p0) with
>   | p0~1 => let H0 := H p0 in let H2 := Hind p0~0 H0 in H2
>   | p0~0 => H p0
>   | 1 => H1
>   end
>      : forall P : positive -> Prop,
>        P 1 ->
>        (forall p : positive, P p -> P (Psucc p)) -> forall p : positive, P p
> 
> Argument scopes are [_ _ _ positive_scope]
> 
> My intention was for the induction to be on p instead of H which isn't even 
> an 
> argument to the lemma or an inductive type, and I don't understand how "H1 
> p" 
> even makes sense, etc.  (This is with Debian 8.3.pl2+dfsg-1.)

This is a bug in the algorithm used for printing fix (when let-in are
involved). The expected result (that you would now obtain if you
download and compile the last version of the v8.3 branch on the svn
repository) is:

Pind2 = 
fix Pind2 (P : positive -> Prop) (H1 : P 1)
          (Hind : forall p : positive, P p -> P (Psucc p))
          (H:=
           fun p : positive =>
           Pind2 (fun p0 : positive => P p0~0) (let H2 := Hind 1 H1 in H2)
             (fun (p0 : positive) (IHp : P p0~0) =>
              let IHp0 := Hind p0~0 IHp in let IHp1 := Hind p0~1 IHp0 in IHp1)
             p) (p : positive) {struct p} : P p :=
  match p as p0 return (P p0) with
  | p0~1 => let H0 := H p0 in let H2 := Hind p0~0 H0 in H2
  | p0~0 => H p0
  | 1 => H1
  end
     : forall P : positive -> Prop,
       P 1 ->
       (forall p : positive, P p -> P (Psucc p)) -> forall p : positive, P p

The use of let-in in the proof does not help in understanding the
proof. After replacing Qed by Defined, you'll get a nicer-looking
proof by diplaying the proof using "Eval lazy zeta beta delta [Pind2]
in Pind2":

fix Pind2 (P : positive -> Prop) (H1 : P 1)
          (Hind : forall p : positive, P p -> P (Psucc p))
          (p : positive) {struct p} : P p :=
         match p as p0 return (P p0) with
         | p0~1 =>
             Hind p0~0
               (Pind2 (fun p1 : positive => P p1~0) 
                  (Hind 1 H1)
                  (fun (p1 : positive) (IHp : P p1~0) =>
                   Hind p1~1 (Hind p1~0 IHp)) p0)
         | p0~0 =>
             Pind2 (fun p1 : positive => P p1~0) (Hind 1 H1)
               (fun (p1 : positive) (IHp : P p1~0) =>
                Hind p1~1 (Hind p1~0 IHp)) p0
         | 1 => H1
         end

Indeed, it is noticeably more direct than the proof of the standard
library (which itself uses the ideas from McBride and McKinna's "The
view from the left"). That's nice.

Hugo Herbelin