ssreflect

Part of coq stdlib. No need of mathcomp

General

• do n! tac apply the tactic tac, n times.

Multipliers

ssrfun

https://coq.inria.fr/doc/V8.18.0/stdlib/Coq.ssr.ssrfun.html

• left_id, right_id
• left_zero, right_zero
• idempotent
• commutative
• left_commutative, right_commutative
• left_distributive, right_distributive
• associative
• injective: ∀x y, f x = f y -> x = y
• left_injective, right_injective
• left_inverse, right_inverse
• involutive
• interchange

ssrbool

• xpredT: Notation for identity function for true
  • As in a predicate that's always true.
• a \in P: P is a predicate and P a holds.
• a \notin P: opposite of a \in P
• predD P Q: elements which are satisfied by P but not by Q
  • As in P \ Q, like set difference.
  • Underlying function is xpredD.
  • Mathcomp syntax: [predD P & Q]

Clear switchᵈ

Introduction with curly braces means at the end of that tactic, the introduced variable will disappear from the set of hypotheses.

rewrite

Probably the most useful tactic.

Tips:

• rewrite within an assumption H as well as the goal: rewrite in H *

Occurrence selection ᵈ

• rewrite {2}<name>: rewrite only 2nd occurrance of name
• rewrites {-2}<name>: rewrite all occurrances of name except the 2nd one

Some 'reflecting' examples

• case/exists_inP is same as move/exists_inP => x; case: x

andP

Require Import ssreflect ssrbool.

Goal
  True -> true && true.
Proof.
  move => H.
(*
1 subgoal

H : True

========================= (1 / 1)

true && true
*)
  apply/andP.
(*
1 subgoal

H : True

========================= (1 / 1)

true /\ true
*)

exists_inP (move)

One with mathcomp:

Check exists_inP.
(*
exists_inP
     : reflect (exists2 x : ?T, ?D x & ?P x) [exists (x | ?D x), ?P x]
where
?T : [ |- finType]
?D : [ |- pred ?T]
?P : [ |- pred ?T]
*)

Goal forall (x:'I_3) (P1 P2: 'I_3 -> bool),
  [exists (x | P2 x), P1 x] -> True.
Proof.
  move => x P1 P2.
(*
1 subgoal

x : 'I_3
P1, P2 : 'I_3 -> bool

========================= (1 / 1)

[exists (x0 | P2 x0), P1 x0] -> True
*)
  move/exists_inP.
(*
1 subgoal

x : 'I_3
P1, P2 : 'I_3 -> bool

========================= (1 / 1)

(exists2 x0 : fintype_ordinal__canonical__fintype_Finite 3, P2 x0 & P1 x0) ->
True
*)

exists_inP (case)

[exists (dst | true), accept eps dst l] -> s :: l \in nilp (T:=A)

case/exists_inP.

forall x : unit, true -> accept eps x l -> s :: l \in nilp (T:=A)

Misc

• An ssreflect library is being developed for Lean as well: https://github.com/verse-lab/lean-ssr/tree/master
• odflt: option default