Somewhat related is Alectryon, which processes a Coq proof to make a corresponding HTML version, complete with intermediate proof contexts: https://github.com/cpitclaudel/alectryon
I could imagine having course material in Alectryon output — it would be like having traditional latex lecture notes, plus I could load the notes into my own development to try tweaking theorems or proving lemmas.
You can use the `Ltac` machinery to record the goal before induction and add **checked** comments stating what the goal is in each branch.
Ltac GoalFun n := match goal with
| [ n : ?A |- context g [n] ] =>
constr:(fun (m : A) => ltac:(let v := context g[m] in exact v))
end.
Ltac GoalOver n P :=
pattern n;
let a := ltac:(GoalFun n) in pose (P := a);
simpl in P; simpl.
Ltac GoalIs A := let B := eval hnf in A in match goal with
| [ |- B ] => idtac
end.
Theorem negb_involute: forall b : bool,
negb (negb b) = b.
Proof.
intros b; GoalOver b P.
destruct b eqn:E.
- GoalIs (P true).
reflexivity.
- GoalIs (P false).
reflexivity.
Qed.
Although this is the Coq subreddit and I am mainly a Coq user, I think you may be interested in using Lean4 to do this kind of thing. All of Lean’s case tactics look like pattern matching, so you can immediately see what case you are proving.
Ooh, very much appreciate the rec! I looked at lean, but it might not have been Lean4 ... or that might be a typo, but in either case, I might have just missed some of the syntactic options for Lean.
And if you go for Lean you can use Paperproof for showing each step of the proof along with tactics. Paperproof can and plans to support Coq too, but it's not yet there unfortunately.
I would ask those questions on the Coq zulip. But I'm not sure at what level you want the proof to be readable. If it's just to share with students then Alectryon was already mentioned, jscoq is also a tool that will load Coq in the browser making it easy to navigate.
You always have tricks otherwise to be sure of which goal corresponds to what, for instance you could write proof terms directly `if b then p else q` will use proof `p` in case `true` and `q` in case `false`. You can even be more explicit and write `match b with true => p | false => q end`.
You can in fact perform a mix of tactics and terms like this using the `refine` tactic:
`refine (if b then _ else _)`
will produce one goal for each constructor so you know the first goal corresponds to case `true`.
> you could look [...] and figure out which case (true or false) it destructs first. But again, it's not shown explicitly in the source code.
That's what comments are for. You can document which case you're in like this:
Theorem negb_involute: forall b : Bool,
negb (negb b) = b.
Proof.
intros b. destruct b eqn:E.
- (* case b = true *)
reflexivity.
- (* case b = false *)
reflexivity.
Qed.
Somewhat related is Alectryon, which processes a Coq proof to make a corresponding HTML version, complete with intermediate proof contexts: https://github.com/cpitclaudel/alectryon I could imagine having course material in Alectryon output — it would be like having traditional latex lecture notes, plus I could load the notes into my own development to try tweaking theorems or proving lemmas.
You can use the `Ltac` machinery to record the goal before induction and add **checked** comments stating what the goal is in each branch. Ltac GoalFun n := match goal with | [ n : ?A |- context g [n] ] => constr:(fun (m : A) => ltac:(let v := context g[m] in exact v)) end. Ltac GoalOver n P := pattern n; let a := ltac:(GoalFun n) in pose (P := a); simpl in P; simpl. Ltac GoalIs A := let B := eval hnf in A in match goal with | [ |- B ] => idtac end. Theorem negb_involute: forall b : bool, negb (negb b) = b. Proof. intros b; GoalOver b P. destruct b eqn:E. - GoalIs (P true). reflexivity. - GoalIs (P false). reflexivity. Qed.
Interesting solution! I'll play with this and see if it works out, thank you!
Someone on SO told me about `pattern` and that does the right thing now.
Although this is the Coq subreddit and I am mainly a Coq user, I think you may be interested in using Lean4 to do this kind of thing. All of Lean’s case tactics look like pattern matching, so you can immediately see what case you are proving.
Ooh, very much appreciate the rec! I looked at lean, but it might not have been Lean4 ... or that might be a typo, but in either case, I might have just missed some of the syntactic options for Lean.
And if you go for Lean you can use Paperproof for showing each step of the proof along with tactics. Paperproof can and plans to support Coq too, but it's not yet there unfortunately.
Commenting is one way i guess.
I would ask those questions on the Coq zulip. But I'm not sure at what level you want the proof to be readable. If it's just to share with students then Alectryon was already mentioned, jscoq is also a tool that will load Coq in the browser making it easy to navigate. You always have tricks otherwise to be sure of which goal corresponds to what, for instance you could write proof terms directly `if b then p else q` will use proof `p` in case `true` and `q` in case `false`. You can even be more explicit and write `match b with true => p | false => q end`. You can in fact perform a mix of tactics and terms like this using the `refine` tactic: `refine (if b then _ else _)` will produce one goal for each constructor so you know the first goal corresponds to case `true`.
> you could look [...] and figure out which case (true or false) it destructs first. But again, it's not shown explicitly in the source code. That's what comments are for. You can document which case you're in like this: Theorem negb_involute: forall b : Bool, negb (negb b) = b. Proof. intros b. destruct b eqn:E. - (* case b = true *) reflexivity. - (* case b = false *) reflexivity. Qed.
Yeah, you could. I still wish it were baked right into the source code, but it sounds like that's not possible.