It seems my coq proofs are longer and uglier than expected and I can't achieve ssreflect advantages in them despite my attempts. I think I missed some key points. Or maybe I just need to know more tactics.
Here are some proofs I came up with. Please, help me to find and fix bad lines or decisions I made. I noted with comments the lines that I doubt. Advice about evidence or sources of knowledge will also be useful.
(* SSReflect proof language requires these libraries to be loaded and options to be set. *)
From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
From Coq Require Import Nat Arith Lia.
Lemma L1: forall A B C, A -> (A -> B /\ C) -> C.
Proof.
move => A B C H1 H2.
(* Seems like there is a way to apply H2 in H1 without moving them from goal. *)
apply H2 in H1.
destruct H1 as [H3 Goal].
done.
Qed.
Lemma L2: forall A Q, (forall x, (exists y, x + y = y + x) -> A) -> Q -> A.
Proof.
move => A _ T _.
(* I think there is a better way then coming up with this "H" or smth. *)
assert (H: exists y, 2 + y = y + 2) by (exists 0; lia).
(* Again, there should be the way to do apply via ssreflect. *)
apply (T 2) in H.
done.
Qed.
Lemma divides_by_2_by_3_means_by_6 :
forall z p q, z = 2 * p -> z = 3 * q -> exists n, z = 6 * n.
Proof.
move => a b c P Q.
(* Which way is better to create a subgoal? *)
assert (odd_or_even: forall n, (exists k, n = 2 * k) \/ (exists k, n = 2 * k + 1)). {
induction n.
- left. exists 0. lia.
- destruct IHn as [[x H] | [x H]].
+ right; exists x; lia.
+ left; exists (x + 1); lia.
}
(* How can I add new fact in context? I found this way, but there should be the right one. *)
move : (odd_or_even c) => H.
destruct H as [[x H] | [x H]].
- exists x; lia.
- lia.
Qed.
If you want to take the best out of ssreflect, you might also consider using the full mathematical components library. But for now, I will just illustrate the tactics, not the theorems. I am a frequent user of ssreflect and mathematical components, so this will also contain some stylistic habits that are enforced in this library (like the convention for indentation, which is 2 * (n - 1) spaces, where n is the number of open goals), and the habit of adding "by" at the beginning of every line that finishers a proof.
From Coq Require Import ssreflect ssrfun ssrbool.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
From Coq Require Import Nat Arith Lia.
Lemma L1: forall A B C, A -> (A -> B /\ C) -> C.
Proof.
by move=> A B C /[swap] /[apply] - [].
Qed.
The \[swap] and \[apply] introduction patterns are fairly recent additions to the language.
Lemma L2: forall A Q, (forall x, (exists y, x + y = y + x) -> A) -> Q -> A.
Proof.
by move=> A _ + _ => /(_ 2); apply; exists 0; lia.
Qed.
In this example note the use of + to express that the hypothesis is kept in the goal, while the next one is discarded by _.
The apply tactic without argument takes its argument as the first proposition on the left of arrows in the goal.
Lemma divides_by_2_by_3_means_by_6 :
forall z p q, z = 2 * p -> z = 3 * q -> exists n, z = 6 * n.
Proof.
have odd_or_even : forall n, (exists k, n = 2 * k) \/
(exists k, n = 2 * k + 1).
elim=> [ | n [[k kP] | [k kP]]]; first by left; exists 0.
by right; exists k; lia.
by left; exists (k + 1); lia.
move=> a b c P Q; move: (odd_or_even c)=> [[x H] | [x H]].
by exists x; lia.
by lia.
Qed.
Here the elim tactic behaves like the apply tactic in the previous example: it takes its argument as the leftmost universally quantified (or premise) on the goal. Introduction patterns are used directly to destruct the hypotheses which are disjunctions or existential statements.
Until recently, mathematical components made little use of lia so this is not completely idiomatic ssreflect code, but it does work. Personnally, I am a bit confused that lia manages to solve the last goal.