Damien Pous' sessions will be given only online, on BBB (classroom M2IF-CR13).
For an exhaustive list, see Coq documentation on tactics (you can look for a specific tactic there).
|intro H. intros HA HAB. intros H [H|H'].||(introduce hypotheses, possibly decomposing them on the fly)|
|apply H. apply H, H'. apply (H H'). apply (te A). apply H in H'.||(apply an hypothesis, a theorem, or a term)|
|assert(H: T). assert(H: T) by tac.||(prove a lemma inside a proof)|
|split. left. right. exists.||(proving a conjunction, a discjunction, an exists)|
| destruct H as [H1 H2]. destruct H as [H1|H2].
destruct H as [x Hx]. destruct (te A) as [HA HnA].
|(decompose an hypothesis or a term)|
|contradict H.||(close the goal by contradicting an hypothesis)|
|assumption.||(close the goal by using one of the hypotheses)|
|reflexivity.||(prove an equality by reflexivity)|
|rewrite H, (plus_comm x). rewrite H in H'. rewrite <- H. rewrite H at 2.||(rewrite using an equality)|
|induction n as [|m IH].||(proceeed by induction on n ( = destruct + induction hypothesis))|
|set (x:=e).||(give a name to a term or a pattern)|
|simpl. simpl in H.||(simplify the goal or an hypothesis by computation)|
|tauto.||(solve a propositional tautology)|
|trivial.||(try simple things such as assumption or reflexivity, leave the goal unchanged if it does not work)|
|easy.||(try simple things such as assumption or reflexivity, fails if this does not solve the goal)|
|ring.||(solve ring equations (polynomials))|
|field.||(solve field equations)|
|field_simplify.||(expand/simplify field expressions)|
|lia.||(linear integer arithmetic - max, plus, minus, le, lt... but not mult)|
|lra.||(linear real arithmetic - idem)|
|tac1; tac2.||(apply tac2 to all subgoals generated by tac1)|
|repeat tac.||(repeatedly apply tac)|
|now tac.||(apply tac and conclude easily (e.g., with assumption))|
|try tac.||(try to apply tac, not complaining if it fails---à consommer avec modération)|
The mathematical background of Coq is the calculus of inductive constructions (CIC), which is an extension of the calculus of constructions (CC), which is an extension of the simply typed lambda calculus.Other related keywords are Martin Löf dependent type theory, the lambda-cube and pure type systems (PTS).
There are three main additions leading from the simply typed lambda calculus to CC:
'a listin OCaml/Haskell)
map: ('a -> 'b) -> 'a list -> 'b listin OCaml/Haskell, and actually a bit more
If you have no background in lambda calculus, I recommend that you read chapters 3, 7, and 11 of Proofs and Types (and also the beginning of chapter 4, not for the proof of normalisation itself, but for understanding what is normalisation).
The above two references are not Coq-specific, but they present precisely the actual theory behind Coq. Then there is the Coq'Art book, which is Coq-specific, but more focused on learning Coq than its underlying theory (still, it might be a very good read, especially the first chapters).
sudo apt remove ocaml* coq* opam*
rm -rf ~/.opam
[sudo add-apt-repository ppa:avsm/ppa] # under ubuntu, the goal is to get opam 2
sudo apt update
sudo apt install ocaml opam
opam init # accept that it setups things in your initialisation files
eval $(opam env)
opam install opam-depext
opam repo add coq-released https://coq.inria.fr/opam/released
opam-depext coq coq-ide coq-interval
# possibly the last command will propose you do do the next step directly
sudo apt install [whatever was listed above]
opam install coq coqide coq-interval
coqtopin a terminal tells you `Welcome to Coq 8.12';
emacs, and then you can repeatedly press the button with a green arrow going down or type
C-c C-band eventually see `Well_done is defined'.