The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Anthony,

 

using automation it is possible with Coq to come to a proof style which is quite similar to what humans usually do: just give a rough sketch and let automation figure out the details. So what I would recommend is this:

 

Create HintDb HdbLocal discriminated.

 

Variable P : nat -> Prop.

 

Axiom P0: P 0.

Hint Resolve P0 : HdbLocal.

 

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

Hint Resolve PSn : HdbLocal.

 

Theorem Pn_1: forall n:nat, P n.

Proof.

  induction n; eauto with HdbLocal.

Qed.

 

I usually get around 95% of my proofs into such a one liner, usually some sort of case analysis tactic, like induction, followed by eauto with some collection of hint databases. Of cause you need to give fine grain enough lemmas so that automation is not too difficult and also hint databases need to be well organized for efficiency. Usually when I create a lemma, I immediately give the automation hints how this lemma is typically applied. This can be a simple Hint Resolve (as above), but sometimes is something more involved like a guarded Hint Extern.

 

I found this proof style to be very readable and maintainable. The book “Certified Programming with Dependent Types” by Adam Chlipala (also available online) gives a good introduction to this style (and is also worth reading for its main topic), although I ended up with quite a different implementation of automation, more based on eauto and hint databases.

 

Best regards,

 

Michael

 

From: anthony.j.towns AT gmail.com [mailto:anthony.j.towns AT gmail.com] On Behalf Of Anthony Towns
Sent: Friday, June 26, 2015 6:29 AM
To: coq-club AT inria.fr
Subject: [Coq-Club] induction with eqn:

 

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>