The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

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