The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Hi,

There are two different features IMHO here:

1) Document the different cases of a proof (see B. Pierce solution here: http://www.cis.upenn.edu/~bcpierce/sf/current/Induction.html#lab38), and:

1bis)  if possible make coq verify this documentation in order to help writing correct doc (Pierce's solution does not this). This is a frequent wish and not currently implemented yet AFAIK.

2) Really generate equalities in the goal and the proof term which is iseful in some cases but not a good way to implement 1) IMHO as it "pollutes" the proof term and environment with (often useless) equalities. 

The challenge is: implement 1bis) without 2).

------------------------

Remarks on your tactic:

match goal with ?FP n =>... 

will only match goals of this form. Doing "pattern n" before will capture a lot more goals.

Moreover it is not clear to me if the part 

match goal with [ |- PROP ?nnn ] => ...

will not capture unwanted hypothesis.

Best,

P.

2015-06-26 6:28 GMT+02:00 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>