The Coq mailing list

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

Pierre Courtieu wrote:

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.

Yep; my Case tactic is based on exactly that one, with the bonus that it explicitly fails unless there's a hypothesis that matches the case statement.

I briefly tried another version as well, which was something like:

Tactic Notation "clevercase" constr(cond) "{" tactic(tac) "}" :=

  match goal with

   | [ |- _ ] => assert cond by auto; (solve [tac] || fail 2 "tactic for" cond "did not succeed")

   | [ |- ?G ] => idtac "skipping tactic for" G "because it's not obvious that" cond

  end.

The idea being you could do things like say:

  destruct (decidable P);

  clevercase (P) { assumption };

  clevercase (~P) { contradiction }.

The theory was that the case tactic itself would choose what goals were focused, so that it wouldn't matter what order you did the cases in. And it also means that if you've got a bunch of cases that can all get proved the same way, you can just specify them together:

  destruct (decidable P); destruct (decidable Q);

  clevercase (P /\ Q) { split; assumption } ;

  clevercase (~P \/ ~Q) { contradiction }

instead of having to be repetitive:

  destruct (decidable P); destruct (decidable Q)

   - split; assumption.

   - contradiction.

   - contradiction.

   - contradiction.

I've given up on that for the moment though because not being able to incrementally write/debug the case proofs is no fun (ie, your tactics have to all be separated by ; not by .)

(The version above doesn't actually let you do the cases in arbitrary order since it fails if it references terms that some of the cases don't have defined -- so you can't do clevercase (n = S n') before clevercase (n = 0) eg).

 

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.

So this is easy for me since I *want* the "pollution" here, because I'm trying to write proofs that both satisfy coq and match the way I'd write them by hand, and I'd have the equalities if I were doing it by hand.

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

I think you'd have to identify your case by a goal and not just a hypothesis if you didn't want to introduce unnecessary equations (because the base inductive cases don't get any hypotheses). But that's pretty easy, isn't it? eg:

Ltac check_case h g := 

  match goal with

   | |- ?G => let H := fresh in 

        assert (h) as H by solve[auto]; clear H;

        assert (g->G) as H by solve[contradiction|auto]; clear H

   | _ => 

        assert (h) by solve[auto]; fail 2 "case does not appear to have" g "as goal"

   | |- ?G =>

        assert (g->G) as H by solve[contradiction|auto]; fail 2 "case does not appear to have" h "as hypothesis"

   | _ => fail 2 "case does not have" h "as hypothesis OR " g "as goal."

  end.

Tactic Notation "Case" constr(p) := check_case p False.

Tactic Notation "Case" "|-" constr(g) := check_case True g.

Tactic Notation "Case" constr(p) "|-" constr(g) := check_case p g.

Theorem Px: forall n:nat, is_even (n + n).

Proof.

  intros n. induction n.

  - Case |- (is_even (0 + 0)). 

    unfold plus, is_even. trivial.

  - Case (is_even (n+n)).

    Case |- (is_even (S n + S n)).

    Case (is_even (n+n)) |- (is_even (S n + S n)).

    rewrite <- plus_n_Sm, plus_Sn_m; unfold is_even; apply IHn.

Qed.

------------------------
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.

Yep, I figured that out shortly after I posted... *sigh*

Moreover it is not clear to me if the part 
match goal with [ |- PROP ?nnn ] => ...
will not capture unwanted hypothesis.

Given I just defined PROP prior to the induction, and I want everything that's a result of the induction, how would it match anything unwanted?

​​

Cheers,

aj

On 26 June 2015 at 14:28, Anthony Towns <aj AT erisian.com.au> wrote:

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>

--

Anthony Towns <aj AT erisian.com.au>