The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sunday 24 April 2011 02:58:52 Hugo Herbelin wrote:
> Hi,

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

Well, it did help for me, in seeing that the recursive call to Pind2 is 
always 
using p/2 as the p argument.  Based on the same principle, I wrote a direct 
definition of Prect2:

Fixpoint Prect2 (P:positive->Type) (a:P 1)
  (f: forall p:positive, P p -> P (Psucc p)) (p:positive) : P p :=
let double_fn := Prect2 (fun p:positive => P (p~0))
  (f _ a) (fun (p:positive) (x:P (p~0)) => f _ (f _ x)) in
match p with
| q~1 => f _ (double_fn q)
| q~0 => double_fn q
| 1 => a
end.

Proposition Prect2_succ: forall P a f (p:positive),
  Prect2 P a f (Psucc p) = f _ (Prect2 P a f p).
Proof.
intros.
revert P a f.
induction p.

intros.
simpl.
rewrite IHp.
reflexivity.

reflexivity.

reflexivity.
Qed.

Proposition Prect2_base: forall P a f, Prect2 P a f 1 = a.
Proof.
reflexivity.
Qed.
-- 
Daniel Schepler