Systems and
Formalisms Lab

Lab 1: Debrief

Author

Dario Halilovic, Clément Pit-Claudel

From Stdlib Require Import Lia Arith String List.
Open Scope N_scope.

Notes on Rocq tactics

apply vs rewrite

These two tactics are almost never interchangeable.

  • apply implements the following rule, which means “to prove B, it's enough to prove A and A → B”

    A A → B B

  • rewrite implements a different rule that means “to prove C, it's enough to prove x = y and C with all x replaced by y”:

    x = y [ y / x ] C C

Use apply when the conclusion of a hypothesis matches the goal:

H: … → conclusion
===================
conclusion

Use rewrite when a hypothesis is an equality about a variable mentionned in the goal:

H: a = …
==================
… a …

Here is a concrete example:

forall (A B : Type) (f : A -> B) (l : list A),
Datatypes.length (map f l) = Datatypes.length l


forall (A B : Type) (f : A -> B) (l : list A),
Datatypes.length (map f l) = Datatypes.length l

  
A, B: Type
f: A -> B
a: A
l: list A
IHl: Datatypes.length (map f l) = Datatypes.length l
S (Datatypes.length (map f l)) =
S (Datatypes.length l)

apply doesn't work out of the box, because the goal doesn't match; we can either use rewrite and equality or f_equal and apply:

   
In environment
A : Type
B : Type
f : A -> B
a : A
l : list A
IHl : Datatypes.length (map f l) = Datatypes.length l
Unable to unify
 "Datatypes.length (map f l) = Datatypes.length l"
with
 "S (Datatypes.length (map f l)) =
  S (Datatypes.length l)".

   
A, B: Type
f: A -> B
a: A
l: list A
IHl: Datatypes.length (map f l) = Datatypes.length l
S (Datatypes.length l) = S (Datatypes.length l)

   reflexivity.
Qed.

Here's how it looks with apply:

forall (A B : Type) (f : A -> B) (l : list A),
Datatypes.length (map f l) = Datatypes.length l


forall (A B : Type) (f : A -> B) (l : list A),
Datatypes.length (map f l) = Datatypes.length l

  
A, B: Type
f: A -> B
a: A
l: list A
IHl: Datatypes.length (map f l) = Datatypes.length l
S (Datatypes.length (map f l)) =
S (Datatypes.length l)


   
Datatypes.length (map f l) = Datatypes.length l

   apply IHl.
Qed.

Implicit quantification in lemma statements

The following two lemmas statements mean the same thing, but they behave slightly differently:

forall i j k : nat, i < j -> j < k -> i < k


forall i j k : nat, i < j -> j < k -> i < k

  
forall j k : nat, 0 < j -> j < k -> 0 < k
i: nat
IHi: forall j k : nat, i < j -> j < k -> i < k
forall j k : nat, S i < j -> j < k -> S i < k
 
i: nat
IHi: forall j k : nat, i < j -> j < k -> i < k
forall j k : nat, S i < j -> j < k -> S i < k

    
IHi
     : forall j k : nat, i < j -> j < k -> i < k

Abort.


i, j, k: nat
i < j -> j < k -> i < k


i, j, k: nat
i < j -> j < k -> i < k

  
j, k: nat
0 < j -> j < k -> 0 < k
i, j, k: nat
IHi: i < j -> j < k -> i < k
S i < j -> j < k -> S i < k
 
i, j, k: nat
IHi: i < j -> j < k -> i < k
S i < j -> j < k -> S i < k

    
IHi
     : i < j -> j < k -> i < k

Abort.

The key difference is that in the second version, i, j, and k are already “introduced”, as if we had run intros, and as a result the induction hypothesis doesn't get forall-quantified over j and k.

induction vs destruct

If you want to perform case analysis on some expression x, use destruct x and not induction x. While the latter will essentially do the same for non-recursive inductive types, the former is much more idiomatic and does what you intended with recursive inductive types. With recursive inductive types, using induction x would add unnecessary induction hypotheses to the environment.

Consider the following example:

forall n : nat, n > 0 -> n - 1 < n


forall n : nat, n > 0 -> n - 1 < n

We want to perform case analysis on n to treat the case n = 0 separately.

  
n: nat
n > 0 -> n - 1 < n
 
0 > 0 -> 0 - 1 < 0
n: nat
IHn: n > 0 -> n - 1 < n
S n > 0 -> S n - 1 < S n

  
0 > 0 -> 0 - 1 < 0
 
ABS: 0 > 0
0 - 1 < 0
 
ABS: 0 < 0
0 - 1 < 0

    
ABS: 0 < 0
False
 
ABS: 0 < 0
0 < 0
 assumption.
  
n: nat
IHn: n > 0 -> n - 1 < n
S n > 0 -> S n - 1 < S n

Performing induction on n adds an unnecessary induction hypothesis to the environment.

Abort.


forall n : nat, n > 0 -> n - 1 < n


forall n : nat, n > 0 -> n - 1 < n

  
n: nat
n > 0 -> n - 1 < n
 
0 > 0 -> 0 - 1 < 0
n: nat
S n > 0 -> S n - 1 < S n

  
0 > 0 -> 0 - 1 < 0
 
ABS: 0 > 0
0 - 1 < 0
 
ABS: 0 < 0
0 - 1 < 0

    
ABS: 0 < 0
False
 
ABS: 0 < 0
0 < 0
 assumption.
  
n: nat
S n > 0 -> S n - 1 < S n

Here, we do not have an unnecessary induction hypothesis in the environment.

    
n: nat
S n - 1 < S n
 
n: nat
n - 0 < S n
 
n: nat
n < S n

    
n: nat
S n <= S n
 reflexivity.
Qed.

Writing better proofs

Consider using bullets or braces to structure your proofs. You can use -, +, and * in order, and if you're using Emacs, they'll be indented automatically.

forall A B : Prop,
A <-> B -> B -> (((A /\ A) /\ A) /\ A /\ A) /\ A


forall A B : Prop,
A <-> B -> B -> (((A /\ A) /\ A) /\ A /\ A) /\ A

  
A, B: Prop
H: A <-> B
H0: B
(((A /\ A) /\ A) /\ A /\ A) /\ A

  
A, B: Prop
H: A <-> B
H0: B
((A /\ A) /\ A) /\ A /\ A
A, B: Prop
H: A <-> B
H0: B
A

  
A, B: Prop
H: A <-> B
H0: B
((A /\ A) /\ A) /\ A /\ A
 
A, B: Prop
H: A <-> B
H0: B
(A /\ A) /\ A
A, B: Prop
H: A <-> B
H0: B
A /\ A

    
A, B: Prop
H: A <-> B
H0: B
(A /\ A) /\ A
 
A, B: Prop
H: A <-> B
H0: B
A /\ A
A, B: Prop
H: A <-> B
H0: B
A

      
A, B: Prop
H: A <-> B
H0: B
A /\ A
 
A, B: Prop
H: A <-> B
H0: B
A
A, B: Prop
H: A <-> B
H0: B
A

        
A, B: Prop
H: A <-> B
H0: B
A
 apply H; assumption. 
A, B: Prop
H: A <-> B
H0: B
A

        
A, B: Prop
H: A <-> B
H0: B
A
 apply H; assumption. }
      
A, B: Prop
H: A <-> B
H0: B
A
 apply H; assumption.
    
A, B: Prop
H: A <-> B
H0: B
A /\ A
 
A, B: Prop
H: A <-> B
H0: B
A
A, B: Prop
H: A <-> B
H0: B
A

      
A, B: Prop
H: A <-> B
H0: B
A
 apply H; assumption. 
A, B: Prop
H: A <-> B
H0: B
A

      
A, B: Prop
H: A <-> B
H0: B
A
 apply H; assumption. }
  
A, B: Prop
H: A <-> B
H0: B
A
 apply H; assumption.
Qed.

Note that the indentation naturally follows the structure of the proof. If you however find yourself needing more than 3 levels of nesting, you should introduce sublemmas—“bullet hell” is a real thing!

When structuring your proofs, you should also aim to factor out common tactics as often as possible using the semi-colon (;) tactical. This can greatly shorten your proofs when all cases are similar enough.

If your cases slightly differ by one tactic, make use of the square brackets ([ | ]) to dispatch tactics to each case:

forall A B : Prop, A \/ B -> B \/ A


forall A B : Prop, A \/ B -> B \/ A

  
A, B: Prop
H: A
B \/ A
A, B: Prop
H: B
B \/ A

  
A, B: Prop
H: A
B \/ A
 
A, B: Prop
H: A
A
 assumption.
  
A, B: Prop
H: B
B \/ A
 
A, B: Prop
H: B
B
 assumption.
Qed.

…can be rewritten as:

forall A B : Prop, A \/ B -> B \/ A


forall A B : Prop, A \/ B -> B \/ A

  intros; destruct H; [ right | left ]; assumption.
Qed.

Bonus trick: when chaining tactics with ;, if only the first goal differs from the others, use [ tac1 | .. ] to apply tac1 to the first goal only.

Manually selecting subgoals

When you have many goals, we do not recommend selecting subgoals manually (don't write 1,3,9,57: reflexivity). It's inelegant, hard to read, and brittle (if goals get ordered differently the wrong goals will get selected).

Instead, if you have many goals, use automation! See this exercise for an example.

Unnecessary steps

Here is a (non-exhaustive) list of steps that can be shortened or removed:

  • simpl and intros are unnecessary before reflexivity.

  • intros x is redundant before destruct/induction x if x was a forall-quantified variable.

  • destruct x; destruct y can be replaced with destruct x, y.

  • try repeat is equivalent to repeat: repeat never fails!

Avoid automatically generated names

Always choose names for your variables/hypotheses: this makes it easier for everyone (including yourself!) to follow your proof at a glance. For example:

forall n m : nat, n <= m -> n * n <= m * m


forall n m : nat, n <= m -> n * n <= m * m

  
n: nat
H: n <= 0
n * n <= 0 * 0
n, m: nat
IHm: n <= m -> n * n <= m * m
H: n <= S m
n * n <= S m * S m

  
n: nat
H: n <= 0
n * n <= 0 * 0
 
n: nat
H: n = 0
n * n <= 0 * 0

    
n: nat
H: n = 0
0 * 0 <= 0 * 0

    constructor.
  
n, m: nat
IHm: n <= m -> n * n <= m * m
H: n <= S m
n * n <= S m * S m
 
n, m: nat
IHm: n <= m -> n * n <= m * m
H: n <= m \/ n = S m
n * n <= S m * S m

    
n, m: nat
IHm: n <= m -> n * n <= m * m
H: n <= m
n * n <= S m * S m
n, m: nat
IHm: n <= m -> n * n <= m * m
H: n = S m
n * n <= S m * S m

    
n, m: nat
IHm: n <= m -> n * n <= m * m
H: n <= m
n * n <= S m * S m
 lia.
    
n, m: nat
IHm: n <= m -> n * n <= m * m
H: n = S m
n * n <= S m * S m
 
n, m: nat
IHm: n <= m -> n * n <= m * m
H: n = S m
S m * S m <= S m * S m

      constructor.
Qed.

…is not easy to read (what's that H hypothesis all about?). Instead, giving names to each hypothesis helps a lot:

forall n m : nat, n <= m -> n * n <= m * m


forall n m : nat, n <= m -> n * n <= m * m

  
n, m: nat
Hn_le_m: n <= m
n * n <= m * m

  
n: nat
Hn_le_m: n <= 0
n * n <= 0 * 0
n, m: nat
Hn_le_m: n <= S m
IHm: n <= m -> n * n <= m * m
n * n <= S m * S m

  
n: nat
Hn_le_m: n <= 0
n * n <= 0 * 0
 
n: nat
Hn_le_m: n = 0
n * n <= 0 * 0

    
n: nat
Hn_le_m: n = 0
0 * 0 <= 0 * 0

    constructor.
  
n, m: nat
Hn_le_m: n <= S m
IHm: n <= m -> n * n <= m * m
n * n <= S m * S m
 
n, m: nat
Hn_le_m: n <= m \/ n = S m
IHm: n <= m -> n * n <= m * m
n * n <= S m * S m

    
n, m: nat
Hn_lt_m: n <= m
IHm: n <= m -> n * n <= m * m
n * n <= S m * S m
n, m: nat
Hn_equals_m: n = S m
IHm: n <= m -> n * n <= m * m
n * n <= S m * S m

    
n, m: nat
Hn_lt_m: n <= m
IHm: n <= m -> n * n <= m * m
n * n <= S m * S m
 lia.
    
n, m: nat
Hn_equals_m: n = S m
IHm: n <= m -> n * n <= m * m
n * n <= S m * S m
 
n, m: nat
Hn_equals_m: n = S m
IHm: n <= m -> n * n <= m * m
S m * S m <= S m * S m

      constructor.
Qed.

Some common tactics, such as destruct, induction or intros, have variants for introducing your own names. A few useful examples:

  • destruct H as [HcaseA | HcaseB] (disjunction case)

  • destruct H as [HA HB] (conjunction case)

  • induction n as [ | IHn]

  • intros (HA & HB & HC)

For more examples, have a look at the reference manual.