The Coq mailing list

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

I was too late to reply (I posted the response I planned to send at
the end of the mail)

but in what should have been generated by Hugo, shouldn't the 
"(H := fun ... => ...)" be inside a "let ... in ..." rather than a
parameter, or did I miss something?

Le Sun, 24 Apr 2011 11:58:52 +0200,
Hugo Herbelin 
<Hugo.Herbelin AT inria.fr>
 a écrit :

> 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

(*
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.
Print Pind2.

(* This is another proof on the same idea,
   but it may make more clear what is done
*)

Lemma Pind3: forall (p:positive) (P:positive->Prop),
  P 1 -> (forall p:positive, P p -> P (Psucc p)) ->
  P p.
Proof.
fix 1.
intros p P H1 Hind.
destruct p.
apply (Pind3 p).
(* always clear "fix" after using it with
   the recursive argument to avoid bad
   surprises later (when you use auto, admit,
   or forgot to check guardedness)

   Note that it is not used with the "P" parameter
   but with the "fun p => P p~1"
*)
clear Pind3.
Guarded.
(* ok, so now we cannot go wrong due to guardedness in
   this branch
*)
apply (Hind 2).
apply (Hind 1).
apply H1.
intros q Hq; generalize (Hind _ Hq).
simpl.
apply Hind.

apply (Pind3 p).
apply (Hind 1).
apply H1.
intros q Hq; generalize (Hind _ Hq).
simpl.
apply Hind.

apply H1.
Qed.
Print Pind3.

(* 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.)
-- 
Daniel Schepler
*)

(* often, one of the first things I do is simplify the
   proof term by rewritting it manually (in fact,
   a copy-paste of the proof term and manual inlining
   and removing of type anotations as well as
   putting some "_"s) *)

(* As it didn't type check, I change the place of the H,
   {struct H} in {struct p} and H1 p in P p;
   maybe is there a bug in the coq printer, as arguments seem
   to have been shifted in a weird maneer *)

Fixpoint Pind4 (P : positive -> Prop) (H1 : P 1)
          (Hind : forall p : positive, P p -> P (Psucc p))
          (p : positive) {struct p} : P p :=
  let H := fun p : positive =>
           Pind4 (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
  in
  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.

(* The after rewrittings I get: *)
Fixpoint Pind5 (P : positive -> Prop) (H1 : P 1)
          (Hind : forall p : positive, P p -> P (Psucc p))
          (p : positive) {struct p} : P p :=
  let H := Pind4 (fun p0 => P p0~0) (Hind 1 H1)
             (fun p0 (IHp : P p0~0) => Hind p0~1 (Hind p0~0 IHp))
  in
  match p as p0 return (P p0) with
  | p0~1 => Hind p0~0 (H p0)
  | p0~0 => H p0
  | 1 => H1
  end.

(* now things should be more clear! *)