The Coq mailing list

[Anthony Towns <aj AT erisian.com.au>]

Hi all,

I discovered coq recently and have been enjoying myself doing some proofs with it, and seeing how "readable" I can make the proof scripts -- by which I mean making it so that you don't have to remember/imagine much of the state of the proof, rather you can just read it. One part of that, I think, is explicitly indicating what case is being examined when splitting the proof up into parts. So I want to be able to write:

  Variable P : nat -> Prop.

  Axiom P0: P 0.

  Axiom PSn : forall n, P n -> P (S n).

  Theorem Pn_1: forall n:nat, P n.

  Proof.

    induction n as [|n'].

    - Case (n = 0).

      apply P0.

    - Case (n = S n').

      apply PSn. exact IHn'.

  Qed. 

​Unfortunately 'induction' doesn't keep 'n' around or introduce an hypothesis deconstructing n; and if I use induction eqn: H, then "n = ..." becomes part of the inductive hypothesis making it unusable. ​I asked on stackoverflow about this [0] and got pointed at a thread from september last year [1], which indicated induction/eqn: is just broken.

But then I had an inspiration -- when doing induction on n, the goal must P(n) for some function P : type(n) -> Prop; and after doing induction, the goal will be P(x) instead, and I can create an hypothesis "n = x" after the induction. And that seems to work:

(* like set (a:=b) except introduces a name and hypothesis *)

Tactic Notation "provide_name" ident(n) "=" constr(v)

       "as" simple_intropattern(H) :=

    assert (exists n, n = v) as [n H] by (exists v; reflexivity).

Tactic Notation

  "induction_eqn" ident(n) "as" simple_intropattern(HNS)

    "eqn:" ident(Hn) :=

  let PROP := fresh in (

    match goal with [ |- ?FP n ] => set ( PROP := FP ) end;

    induction n as HNS;

    match goal with [ |- PROP ?nnn ] => provide_name n = nnn as Hn end;

    unfold PROP in *; clear PROP

  ).

Tactic Notation "Case" constr(prop) :=

  lazymatch goal with

   | [ H: prop |- _ ] => idtac

   | _ => fail "looking at a different case than" prop

  end.

Theorem Pn_2: forall n:nat, P n.

Proof.

  intros n.

  induction_eqn n as [|n'] eqn: Hn.

  - Case (n = 0).

    apply P0.

  - Case (n = S n').

    apply PSn. exact IHn'.

Qed.

Does that seem like a reasonable approach? Could "induction .. eqn:" be made to use that approach and actually work right? Or is it going to fail for more complicated types/induction rules, or more complicated propositions or similar?

Cheers,

aj

​[0] ​http://stackoverflow.com/questions/31049657/in-coq-how-to-do-induction-n-eqn-hn-in-a-way-that-doesnt-mess-up-the-induct

​[1] ​https://sympa.inria.fr/sympa/arc/coq-club/2014-09/msg00060.html

--

Anthony Towns <aj AT erisian.com.au>