Modelling and automation

Authors:

Yannick Forster

Théo Winterhalter

Files:
From Stdlib Require Import Lia List ZArith.
Import ListNotations.

Records

In Rocq you can write structures using what we call "records". They consist of various fields that each contain data of a given type.

For instance, a (bad) type of rationals:

Record bad_rational1 := {
  numerator : nat ;
  denominator : nat
}.

Under the hood, Rocq will define an inductive type with one constructor called Build_bad_rational1.

Record bad_rational1 : Set := Build_bad_rational1
  { numerator : nat;  denominator : nat }.

Arguments Build_bad_rational1 (numerator denominator)%_nat_scope
Arguments numerator b
Arguments denominator b


Build_bad_rational1 : nat -> nat -> bad_rational1

Build_bad_rational1 is not universe polymorphic
Arguments Build_bad_rational1 (numerator denominator)%_nat_scope
Expands to: Constructor lesson4_part1.Build_bad_rational1
Declared in toplevel input, characters 114-127

We can produce values as follows:

Definition half := {|
  numerator := 1 ;
  denominator := 2
|}.

The names of the fields also correspond to what we call projections. They let us access the various values of a record.

= 1
: nat


= 2
: nat


Record bad_rational2 := {
  numerator' : Z ;
  denominator' : nat
}.

We need to give different names because numerator is a global definition.

We can also produce values interactively.

bad_rational2


bad_rational2

constructor will ask us to provide the values for all the fields

  
Z
nat

  
Z
 exact 1%Z.
  
nat
 exact 4.
Defined.

Record rational := {
    numerator'' : Z ;
    denominator'' : nat ;
    den_not_zero : denominator'' <> 0
  }.


Build_rational :
Z -> forall denominator'' : nat, denominator'' <> 0 -> rational

Build_rational is not universe polymorphic
Arguments Build_rational numerator''%_Z_scope denominator''%_nat_scope
  den_not_zero
Expands to: Constructor lesson4_part1.Build_rational
Declared in toplevel input, characters 584-592



quarter = {| numerator' := 1; denominator' := 4 |}
     : bad_rational2

We can also produce values interactively.

rational


rational

  
Z
?Goal0 <> 0

refine will turn arguments that can be derived from other arguments into so-called existential variables (evars)

Abort.

rational

the tactic constructor fails because it cannot introduce evars

  
The command has indeed failed with message:
Unable to find an instance for the variable denominator''.
rational

econstructor can

  
Z
?denominator'' <> 0

Abort.

rational

same for apply:

  
The command has indeed failed with message:
Unable to find an instance for the variable denominator''.
rational

eapply works

  
Z
?denominator'' <> 0

  
Z
 exact 1%Z.
  
?denominator'' <> 0
 
H: 4 <> 0
?denominator'' <> 0

    exact H.
Abort.

rational

   
?denominator'' <> 0

   
4 <> 0
 lia.
Abort.

rational

  
4 <> 0

  lia.
Defined.

Actually, products, which we defined using an inductive type, can also be defined as records. For this we use parameters to records. They work like inductive parameters.

In fact, records are syntactic sugar over inductive types with one constructor that takes all the fields as arguments, and we can even give a name to that constructor.

Record prod' (A B : Type) := mkpair {
  fst' : A ;
  snd' : B
}.

Definition some_pair := mkpair _ _ 12 bool.

some_pair = {| fst' := 12; snd' := bool |}
     : prod' nat Set

Actually it's annoying to have the underscores in mkpair _ _ 12 bool; we're going to change that with the Arguments command.

Arguments mkpair {A B}.

Definition some_other_pair := mkpair false true.

You can also do pattern matching using this constructor.

Definition to_prod {A B} (p : prod' A B) : A * B :=
  match p with
  | mkpair a b => (a, b)
  end.

Since there is only one constructor, we can also use let.

Definition to_prod_alt {A B} (p : prod' A B) : A * B :=
  let 'mkpair a b := p in (a, b).

We can also use a more generic notation that doesn't require remembering the name of mkpair. It's maybe not as explicit so it's up to you to decide which version you prefer.

Definition to_prod_alt2 {A B} (p : prod' A B) : A * B :=
  let (a, b) := p in (a, b).

Generally, one uses the projections directly. They take the parameters as arguments so for convenience we declare them as implicit.

Arguments fst' {A B}.
Arguments snd' {A B}.

Definition to_prod_alt3 {A B} (p : prod' A B) : A * B :=
  (fst' p, snd' p).
Exercise: Projections

Show that to_prod and to_prod_alt3 produce the same result.

forall (A B : Type) (p : prod' A B), to_prod p = to_prod_alt3 p


forall (A B : Type) (p : prod' A B), to_prod p = to_prod_alt3 p

Admitted.

We can use records to represent more complex mathematical structures. See for instance the following record representing monoids.

Record monoid := {
  m_ty : Type ;
  m_ne : m_ty ;
  m_op : m_ty -> m_ty -> m_ty ;
  m_l_ne : forall x, m_op m_ne x = x ;
  m_r_ne : forall x, m_op x m_ne = x ;
  m_assoc : forall x y z, m_op (m_op x y) z = m_op x (m_op y z)
}.

Again we can build these structures interactively using refine.

monoid


monoid

  
forall x : nat, 0 + x = x
forall x : nat, x + 0 = x
forall x y z : nat, x + y + z = x + (y + z)

  
forall x : nat, 0 + x = x
 
x: nat
0 + x = x
 reflexivity.
  
forall x : nat, x + 0 = x
 
x: nat
x + 0 = x
 
x: nat
x = x
 reflexivity.
  
forall x y z : nat, x + y + z = x + (y + z)
 
x, y, z: nat
x + y + z = x + (y + z)
 
x, y, z: nat
x + y + z = x + y + z
 reflexivity.
Defined.

We need Defined to access the fields!

= 0
: m_ty nat_monoid

Notation for m_ne nat_monoid

m_op nat_monoid
     : m_ty nat_monoid -> m_ty nat_monoid -> m_ty nat_monoid

We can prove things generically about monoids.

Notation "a ** b" := (m_op _ a b) (at level 11, left associativity).


m_assoc
     : forall (m : monoid) (x y z : m_ty m), x ** y ** z = x ** (y ** z)



forall (M : monoid) (x y : m_ty M), x ** m_ne M ** y = x ** y


forall (M : monoid) (x y : m_ty M), x ** m_ne M ** y = x ** y

  
M: monoid
x, y: m_ty M
x ** m_ne M ** y = x ** y

More complicated than necessary of course

  
M: monoid
x, y: m_ty M
x ** (m_ne M ** y) = x ** y
 
M: monoid
x, y: m_ty M
x ** y = x ** y
 reflexivity.
Qed.


forall x y : nat, x + 0 + y = x + y


forall x y : nat, x + 0 + y = x + y

  
x, y: nat
x + 0 + y = x + y

  apply monoid_fact with (M := nat_monoid).
Qed.
Exercise: Groups as records

Define a record for groups, building on the record for monoids. Then show that monoid_fact also holds in groups.

monoid_fact
     : forall (M : monoid) (x y : m_ty M), x ** m_ne M ** y = x ** y
Exercise: Lists form a monoid

Show that lists form a monoid using ++ as operation. How does monoid_fact translate to lists? Note that, unlike ** or +, ++ associates to the right, meaning x ++ y ++ z stands for x ++ (y ++ z).

A: Type
monoid


A: Type
monoid

Admitted.


forall (A : Type) (x y : list A), (x ++ []) ++ y = x ++ y


forall (A : Type) (x y : list A), (x ++ []) ++ y = x ++ y

Admitted.

Products of monoids also yield a monoid.

M1, M2: monoid
monoid


M1, M2: monoid
monoid

  
M1, M2: monoid
forall x : m_ty M1 * m_ty M2,
(let '(u, v) := x in (m_ne M1 ** u, m_ne M2 ** v)) = x
M1, M2: monoid
forall x : m_ty M1 * m_ty M2,
(let '(x0, y) := x in fun '(u, v) => (x0 ** u, y ** v)) (m_ne M1, m_ne M2) =
x
M1, M2: monoid
forall x y z : m_ty M1 * m_ty M2,
(let
 '(x0, y0) := (let '(x0, y0) := x in fun '(u, v) => (x0 ** u, y0 ** v)) y in
  fun '(u, v) => (x0 ** u, y0 ** v)) z =
(let '(x0, y0) := x in fun '(u, v) => (x0 ** u, y0 ** v))
  ((let '(x0, y0) := y in fun '(u, v) => (x0 ** u, y0 ** v)) z)

  
M1, M2: monoid
forall x : m_ty M1 * m_ty M2,
(let '(u, v) := x in (m_ne M1 ** u, m_ne M2 ** v)) = x
 
M1, M2: monoid
x: m_ty M1
y: m_ty M2
(m_ne M1 ** x, m_ne M2 ** y) = (x, y)
 
M1, M2: monoid
x: m_ty M1
y: m_ty M2
(x, y) = (x, y)
 reflexivity.
  
M1, M2: monoid
forall x : m_ty M1 * m_ty M2,
(let '(x0, y) := x in fun '(u, v) => (x0 ** u, y ** v)) (m_ne M1, m_ne M2) =
x
 
M1, M2: monoid
x: m_ty M1
y: m_ty M2
(x ** m_ne M1, y ** m_ne M2) = (x, y)
 
M1, M2: monoid
x: m_ty M1
y: m_ty M2
(x, y) = (x, y)
 reflexivity.
  
M1, M2: monoid
forall x y z : m_ty M1 * m_ty M2,
(let
 '(x0, y0) := (let '(x0, y0) := x in fun '(u, v) => (x0 ** u, y0 ** v)) y in
  fun '(u, v) => (x0 ** u, y0 ** v)) z =
(let '(x0, y0) := x in fun '(u, v) => (x0 ** u, y0 ** v))
  ((let '(x0, y0) := y in fun '(u, v) => (x0 ** u, y0 ** v)) z)
 
M1, M2: monoid
x: m_ty M1
y: m_ty M2
u: m_ty M1
v: m_ty M2
a: m_ty M1
b: m_ty M2
(x ** u ** a, y ** v ** b) = (x ** (u ** a), y ** (v ** b))
 
M1, M2: monoid
x: m_ty M1
y: m_ty M2
u: m_ty M1
v: m_ty M2
a: m_ty M1
b: m_ty M2
(x ** (u ** a), y ** (v ** b)) = (x ** (u ** a), y ** (v ** b))
 reflexivity.
Defined.

Type classes

Say we want to use our monoid_fact on pairs of natural numbers. We can write the following:

monoid_fact (prod_monoid nat_monoid nat_monoid)
     : forall x y : m_ty (prod_monoid nat_monoid nat_monoid),
       x ** m_ne (prod_monoid nat_monoid nat_monoid) ** y = x ** y

But this doesn't tell us much. If we want to write it by hand, it actually doesn't really work because Rocq can't find the monoid structure on its own.

The command has indeed failed with message:
In environment
a : nat
b : nat
c : nat
d : nat
The term "(a, b)" has type "(nat * nat)%type"
while it is expected to have type "m_ty ?m0".



forall a b c d : nat, (a, b) ** (0, 0) ** (c, d) = (a, b) ** (c, d)


forall a b c d : nat, (a, b) ** (0, 0) ** (c, d) = (a, b) ** (c, d)

It prints in a readable way, but we had to suffer to write our lemma!

  
a, b, c, d: nat
(a, b) ** (0, 0) ** (c, d) = (a, b) ** (c, d)

  apply monoid_fact.
Qed.

The solution to this problem is called classes. It adapts the notion of type classes one finds in functional programming languages such as Haskell.

Syntax is the same as for records but it is registered as a special structure for Rocq. We move the carrier, neutral and operation as parameters because Rocq will use them to guess which monoid structure we mean.

Class Monoid (A : Type) (neu : A) (op : A -> A -> A) := {
  mon_left_neutral : forall x, op neu x = x ;
  mon_right_neutral : forall x, op x neu = x ;
  mon_assoc : forall x y z, op (op x y) z = op x (op y z)
}.

Instance is a special command for definitions that register them as things Rocq will use automatically if it has to find a value for Monoid nat 0 plus.

Don't worry too much about the export thing. This is called an attribute and it just means that if someone imports the file, then the instance will still be available. We could instead use #[local] to restrict the instance to the module. It does not matter for the course.

Monoid nat 0 Init.Nat.add


Monoid nat 0 Init.Nat.add

  
forall x : nat, 0 + x = x
forall x : nat, x + 0 = x
forall x y z : nat, x + y + z = x + (y + z)

  
forall x : nat, 0 + x = x
 
x: nat
0 + x = x
 reflexivity.
  
forall x : nat, x + 0 = x
 
x: nat
x + 0 = x
 lia.
  
forall x y z : nat, x + y + z = x + (y + z)
 
x, y, z: nat
x + y + z = x + (y + z)
 lia.
Qed.

A lemma we can prove using only the monoid structure on (ℕ,0,+). See how Rocq infers which proofs we are talking about.

forall k n m : nat, k + n + m + 0 = k + (n + m)


forall k n m : nat, k + n + m + 0 = k + (n + m)

  
k, n, m: nat
k + n + m + 0 = k + (n + m)

  
k, n, m: nat
k + n + m = k + (n + m)

  
k, n, m: nat
k + (n + m) = k + (n + m)
 reflexivity.
Qed.

We can prove it in general on monoids with the same proof.

forall (M : Type) (neu : M) (op : M -> M -> M),
Monoid M neu op -> forall k n m : M, op (op (op k n) m) neu = op k (op n m)


forall (M : Type) (neu : M) (op : M -> M -> M),
Monoid M neu op -> forall k n m : M, op (op (op k n) m) neu = op k (op n m)

  
M: Type
neu: M
op: M -> M -> M
H: Monoid M neu op
k, n, m: M
op (op (op k n) m) neu = op k (op n m)

  
M: Type
neu: M
op: M -> M -> M
H: Monoid M neu op
k, n, m: M
op (op k n) m = op k (op n m)

  
M: Type
neu: M
op: M -> M -> M
H: Monoid M neu op
k, n, m: M
op k (op n m) = op k (op n m)
 reflexivity.
Qed.


forall k n m : nat, k + n + m + 0 = k + (n + m)


forall k n m : nat, k + n + m + 0 = k + (n + m)

  
k, n, m: nat
k + n + m + 0 = k + (n + m)
 
k, n, m: nat
Monoid nat 0 Init.Nat.add

Rocq can use type class search to find instances on its own when we use _

  exact _.
Qed.
Exercise: Product instance

Complete the product instance.

forall (A B : Type) (na : A) (nb : B) (opa : A -> A -> A) (opb : B -> B -> B),
Monoid A na opa ->
Monoid B nb opb ->
Monoid (A * B) (na, nb) (fun '(xa, xb) '(ya, yb) => (opa xa ya, opb xb yb))


forall (A B : Type) (na : A) (nb : B) (opa : A -> A -> A) (opb : B -> B -> B),
Monoid A na opa ->
Monoid B nb opb ->
Monoid (A * B) (na, nb) (fun '(xa, xb) '(ya, yb) => (opa xa ya, opb xb yb))

Admitted.

Now you can see that Rocq can infer complex monoid structures on its own!

Definition foo : Monoid (nat * nat * nat) _ _ := _.

foo =
MonoidProd (nat * nat) nat (0, 0) 0
  (fun '(xa, xb) '(ya, yb) => (xa + ya, xb + yb)) Init.Nat.add
  (MonoidProd nat nat 0 0 Init.Nat.add Init.Nat.add MonoidNat MonoidNat)
  MonoidNat
     : Monoid (nat * nat * nat) (0, 0, 0)
         (fun '(xa, xb) '(ya, yb) =>
          ((fun '(xa0, xb0) '(ya0, yb0) => (xa0 + ya0, xb0 + yb0)) xa ya,
           xb + yb))
Exercise: Monoid instance for lists

Define an instance for lists and apply test_monoid to it. Then check that Rocq can now find a monoid structure on list bool * nat * list nat.

Hint: If asked for an instance of Monoid, you can always write exact _. It will trigger class resolution and find it automatically (if you have a corresponding instance).

test_monoid
     : forall (M : Type) (neu : M) (op : M -> M -> M),
       Monoid M neu op ->
       forall k n m : M, op (op (op k n) m) neu = op k (op n m)



forall A : Type, Monoid (list A) [] (app (A:=A))


forall A : Type, Monoid (list A) [] (app (A:=A))

Admitted.


forall (A : Type) (k n m : list A), ((k ++ n) ++ m) ++ [] = k ++ n ++ m


forall (A : Type) (k n m : list A), ((k ++ n) ++ m) ++ [] = k ++ n ++ m

Admitted.

Here is another example of a class: decidable equality.

Class Eq A := {
  eqb : A -> A -> bool ;
  eqb_iff : forall x y, eqb x y = true <-> x = y
}.

Note: `` {Eq A} ` is short for {_ : Eq A} -- i.e. we don't have to give it a name. Indeed we don't care about the name of the instance because we don't need to refer to it explicitly, Rocq finds it on its own.

Fixpoint memb {A} `{Eq A} (x : A) (l : list A) : bool :=
  match l with
  | [] => false
  | y :: l => eqb x y || memb x l
  end.


Nat.testbit: nat -> nat -> bool
Nat.leb: nat -> nat -> bool
Nat.ltb: nat -> nat -> bool
RingMicromega.ge_bool: nat -> nat -> bool
Init.Nat.testbit: nat -> nat -> bool
Init.Nat.ltb: nat -> nat -> bool
Nat.eqb: nat -> nat -> bool
Init.Nat.eqb: nat -> nat -> bool
Init.Nat.leb: nat -> nat -> bool
Nat.testbit_eqf:
  Morphisms.Proper (Morphisms.respectful eq Nat.eqf) Nat.testbit
Nat.eqb_compat:
  Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq))
    Nat.eqb
Nat.testbit_wd:
  Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq))
    Nat.testbit
(use "About" for full details on the implicit arguments of Nat.eqb_compat)

Another useful tool is the refine attribute that also lets us give only partial instances. Note that it only works for Instance, not Definition.

forall x y : nat, (x =? y) = true <-> x = y


forall x y : nat, (x =? y) = true <-> x = y

  
Nat.eqb_refl: forall x : nat, (x =? x) = true
Nat.eqb_spec: forall x y : nat, reflect (x = y) (x =? y)
Nat.eqb_sym: forall x y : nat, (x =? y) = (y =? x)
Nat.eqb_eq: forall n m : nat, (n =? m) = true <-> n = m
Nat.eqb_compare:
  forall x y : nat,
  (x =? y) = match x ?= y with
             | Datatypes.Eq => true
             | _ => false
             end
Nat.eqb_neq: forall x y : nat, (x =? y) = false <-> x <> y
Nat.eqb_compat:
  Morphisms.Proper (Morphisms.respectful eq (Morphisms.respectful eq eq))
    Nat.eqb
Nat.bit0_eqb: forall a : nat, Nat.testbit a 0 = (a mod 2 =? 1)
Nat.pow2_bits_eqb: forall n m : nat, Nat.testbit (2 ^ n) m = (n =? m)
Nat.setbit_eqb:
  forall a n m : nat,
  Nat.testbit (Nat.setbit a n) m = ((n =? m) || Nat.testbit a m)%bool
Nat.clearbit_eqb:
  forall a n m : nat,
  Nat.testbit (Nat.clearbit a n) m = (Nat.testbit a m && negb (n =? m))%bool
Nat.testbit_eqb: forall a n : nat, Nat.testbit a n = ((a / 2 ^ n) mod 2 =? 1)
(use "About" for full details on the implicit arguments of Nat.eqb_compat)
forall x y : nat, (x =? y) = true <-> x = y

  apply Nat.eqb_eq.
Defined.

We still need to use Defined though.

= false
: bool


= true
: bool



= true
: bool


= false
: bool
Exercise: Specification of memb

Give memb a specification using the In predicate and show it correct with respect to it.

memb
     : nat -> list nat -> bool
Exercise: Groups as a class

Define a class of groups and show uniqueness of neutral and inverse for all groups.

Apply this result to a group of your choosing (you will have to provide an instance). To apply a lemma, sometimes apply is not enough. In this case you can use eapply which is more permissive. It creates existential variables (starting with a question mark) corresponding to values it couldn't guess. They are typically resolved as you prove the various goals.

Can you show that every group forms a monoid (again, provide a generic instance)?

Automation

Classes are one form of automation. There are others in Rocq, the main one being tactics. Indeed they can be used to derive properties automatically. We will start by looking again at the In predicate.

We'll start by proving some easy lemmas.

forall (A : Type) (x : A) (l : list A), In x (x :: l)


forall (A : Type) (x : A) (l : list A), In x (x :: l)

  
A: Type
x: A
l: list A
In x (x :: l)

  
A: Type
x: A
l: list A
x = x \/ In x l
 
A: Type
x: A
l: list A
x = x
 reflexivity.
Ok, this we already know, but we can use the auto tactic to deal with

some of this.

Abort.

forall (A : Type) (x : A) (l : list A), In x (x :: l)


forall (A : Type) (x : A) (l : list A), In x (x :: l)

  
A: Type
x: A
l: list A
In x (x :: l)

  
A: Type
x: A
l: list A
x = x \/ In x l
 auto.
Qed.


forall (A : Type) (x y : A) (l : list A), In x l -> In x (y :: l)


forall (A : Type) (x y : A) (l : list A), In x l -> In x (y :: l)

  
A: Type
x, y: A
l: list A
h: In x l
In x (y :: l)

  
A: Type
x, y: A
l: list A
h: In x l
y = x \/ In x l
 auto.
Qed.

Now we would like auto to deal with In without the need to use simpl. It should also be able to deal with more complex examples like the following.

forall (A : Type) (x a b c d : A) (l : list A),
In x l -> In x (a :: b :: c :: d :: l)


forall (A : Type) (x a b c d : A) (l : list A),
In x l -> In x (a :: b :: c :: d :: l)

  
A: Type
x, a, b, c, d: A
l: list A
h: In x l
In x (a :: b :: c :: d :: l)

  
A: Type
x, a, b, c, d: A
l: list A
h: In x l
In x (a :: b :: c :: d :: l)

You can see it does nothing.

  
A: Type
x, a, b, c, d: A
l: list A
h: In x l
In x (b :: c :: d :: l)
 
A: Type
x, a, b, c, d: A
l: list A
h: In x l
In x (c :: d :: l)

This is annoying; let's use repeat:

  
A: Type
x, a, b, c, d: A
l: list A
h: In x l
In x l

  auto.
Abort.

We don't need this lemma, so I abort in order not to save it.

Applying the lemma by hand is not very nice, and rather tedious. We're going to declare hints so that auto knows how to use them.

In fact, we're first going to declare a new database of hints dedicated to In. We call it indb, because why not?

Create HintDb indb.

We then add hints to the database using the Hint Resolve command. Like for instances, we need to specify a locality. It doesn't matter so we're going to go with export as before. We then give it the name of a definition (or lemma etc.) and after the colon the databases to which we want to add the hint.

#[export] Hint Resolve In_hd : indb.


forall (A : Type) (x : A) (l : list A), In x (x :: l)


forall (A : Type) (x : A) (l : list A), In x (x :: l)

  
A: Type
x: A
l: list A
In x (x :: l)

  
A: Type
x: A
l: list A
In x (x :: l)

It still doesn't work, because auto doesn't use indb by default.

  auto with indb.

Now it does!

Abort.

If we do not use a HintDb Rocq automatically uses core, but this behaviour is deprecated and will be removed. Instead, one should do so explicitly:

#[export] Hint Resolve In_hd : core.
Exercise: Extending the hint database

Expand the database so that auto with indb is enough to solve the following goals.

Note: Goal is like Lemma but it doesn't require a name. You won't be able to reuse the proven goal afterwards, but it's useful to test things.

Recall the following lemmas from the lecture.

In_hd
     : forall (A : Type) (x : A) (l : list A), In x (x :: l)


In_tl
     : forall (A : Type) (x y : A) (l : list A), In x l -> In x (y :: l)
forall (A : Type) (x a b c d : A) (l : list A),
In x l -> In x (a :: b :: c :: d :: l)


forall (A : Type) (x a b c d : A) (l : list A),
In x l -> In x (a :: b :: c :: d :: l)

Admitted.


forall (A : Type) (x a b c d : A) (l : list A),
In x (a :: b :: x :: c :: d :: l)


forall (A : Type) (x a b c d : A) (l : list A),
In x (a :: b :: x :: c :: d :: l)

Admitted.
Exercise: Membership in concatenations

Show that In x l implies In x (l ++ r) and that In x r implies In x (l ++ r).

Now add both lemmas to indb. For the first time, we are introducing a choice for auto: presented with the goal In x (l ++ r) it has to choose whether to go left or right. It has no way to know in advance which one is better so it will pick one and backtrack if it doesn't work.

Use it to solve the following two goals.

forall (A : Type) (x : A) (l r : list A), In x l -> In x (l ++ r)


forall (A : Type) (x : A) (l r : list A), In x l -> In x (l ++ r)

Admitted.


forall (A : Type) (x : A) (l r : list A), In x r -> In x (l ++ r)


forall (A : Type) (x : A) (l r : list A), In x r -> In x (l ++ r)

Admitted.
forall (A : Type) (x a b c d : A) (l l' : list A),
In x l -> In x ([a; b; c] ++ l' ++ d :: l)


forall (A : Type) (x a b c d : A) (l l' : list A),
In x l -> In x ([a; b; c] ++ l' ++ d :: l)

Admitted.


forall (A : Type) (x a b c d : A) (l l' : list A),
In x l -> In x (l ++ [a; b; c] ++ l' ++ [d])


forall (A : Type) (x a b c d : A) (l l' : list A),
In x l -> In x (l ++ [a; b; c] ++ l' ++ [d])

Admitted.
Exercise: Equal elements

What if the element in my list is not syntactically what I'm looking for but only equal to it?

Prove a lemma for this particular case and add a hint for it. It should solve the following goal.

forall (A : Type) (x y a b c d : A) (l l' : list A),
x = y -> In x ([a; b; c] ++ l' ++ d :: y :: l)


forall (A : Type) (x y a b c d : A) (l l' : list A),
x = y -> In x ([a; b; c] ++ l' ++ d :: y :: l)

Admitted.

Domain-specific automation tactics

  • lia

For linear integer arithmetic. Solves goals about nat / Z and addition, sometimes multiplication.

  • congruence

For equality. Solves goals about equality, knows about injectivity and disjointness of constructors.

  • tauto

For propositional logic. Solves (intuitionistic) propositional tautologies.

However, it's easy to use it for classical propositional logic as well:

Axiom DNE : forall P : Prop, ~~ P -> P.


forall p : Prop, p \/ ~ p


forall p : Prop, p \/ ~ p

  
p: Prop
p \/ ~ p
 
The command has indeed failed with message:
Tactic failure: tauto failed.
p: Prop
p \/ ~ p
 
p: Prop
~ ~ (p \/ ~ p)
 tauto.
Defined.

Or without manual work

From Stdlib Require Import Classical.


forall p : Prop, p \/ ~ p


forall p : Prop, p \/ ~ p

  
p: Prop
p \/ ~ p
 tauto.
Defined.

  • intuition / firstorder

Uses the tauto algorithm and calls a tactic on the leaves. tauto is intuition fail, i.e. no leaves allowed. intuition is intuition auto with core

Exercise: The arith database

The equality in the exercise "Equal elements" is not always going to be an assumption in the context. But it could be handled by some more automation. There is for instance the arith database that can deal with arithmetic.

You can give two (or more) databases to auto. Check that it indeed succeeds in the following goal with arith but not without.

forall (a b c d : nat) (l l' : list nat),
In (a + b) ([b; c] ++ l' ++ d :: b + a :: l)


forall (a b c d : nat) (l l' : list nat),
In (a + b) ([b; c] ++ l' ++ d :: b + a :: l)

Admitted.
Exercise: Limits of arith

Sadly, it has its limits: check that it isn't sufficient for the following goal even though you should be able to prove it (do it).

Hint: lia is stronger than auto with arith on that one.

forall (a b c d : nat) (l l' : list nat),
In (a + b + c) ([a; b; c] ++ l' ++ d :: c + 0 + a + b :: l)


forall (a b c d : nat) (l l' : list nat),
In (a + b + c) ([a; b; c] ++ l' ++ d :: c + 0 + a + b :: l)

Admitted.
Exercise: Using lia in auto (advanced)

There is a way to use lia with auto actually. For this we have to provide a different kind of hint. Using the command Hint Extern we can tell Rocq what tactic to try when encountering a goal of the form n = m where n, m : nat.

Below what we do is say that when the goal is of the shape @eq nat _ _ then we apply lia. We add this to indb. The 3 is something called cost. auto is actually cost-based and each action it takes has a cost attached to it. auto will start by picking the actions with the lowest cost when it has a choice. When it runs out of money, it gives up.

Check that you can solve the previous goal using auto with indb. Can you also make it so that the other goal works?

#[export] Hint Extern 3 (@eq nat _ _) => lia : indb.


forall (a b c d : nat) (l l' : list nat),
In (a + b + c) ([a; b; c] ++ l' ++ d :: c + 0 + a + b :: l)


forall (a b c d : nat) (l l' : list nat),
In (a + b + c) ([a; b; c] ++ l' ++ d :: c + 0 + a + b :: l)

Admitted.
forall (a b c d : Z) (l l' : list Z),
In (a + b + c)%Z ([a; b; c] ++ l' ++ d :: (c + d + 0 + a - d + b)%Z :: l)


forall (a b c d : Z) (l l' : list Z),
In (a + b + c)%Z ([a; b; c] ++ l' ++ d :: (c + d + 0 + a - d + b)%Z :: l)

Admitted.

Existential variables

We have seen eapply already. But many tactics come with an e version. One such example is the eexists tactic that is very convenient. See below.

forall n : nat, n = 0 \/ (exists m : nat, n = S m)


forall n : nat, n = 0 \/ (exists m : nat, n = S m)

  
n: nat
n = 0 \/ (exists m : nat, n = S m)

  
0 = 0 \/ (exists m : nat, 0 = S m)
n: nat
S n = 0 \/ (exists m : nat, S n = S m)

  
0 = 0 \/ (exists m : nat, 0 = S m)
 auto.
  
n: nat
S n = 0 \/ (exists m : nat, S n = S m)
 
n: nat
exists m : nat, S n = S m
 
n: nat
S n = S ?m
 reflexivity.
We're going to show the proof to see what value was picked for the

existential variable.

  
(fun n : nat =>
 match n as n0 return n0 = 0 \/ (exists m : nat, n0 = S m) with
 | 0 => or_introl eq_refl
 | S n0 =>
     (fun n1 : nat =>
      or_intror (ex_intro (fun m : nat => S n1 = S m) n1 eq_refl)) n0
 end)

Qed.
Exercise: Existential variables

Solve the following goal without using any lemma or variable in the context explicitly.

forall (A : Type) (x : A) (l l' : list A), exists y : A, In y (l ++ x :: l')


forall (A : Type) (x : A) (l l' : list A), exists y : A, In y (l ++ x :: l')

Admitted.

auto also has an eauto variant. You can use it when applying a hypothesis requires guessing a variable that doesn't appear in the goal (like y below). It is generally slower than auto so you can use it when auto fails.

forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
P 4 2 -> (forall x y : nat, P x y -> Q x) -> Q 4


forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
P 4 2 -> (forall x y : nat, P x y -> Q x) -> Q 4

  
P: nat -> nat -> Prop
Q: nat -> Prop
hP: P 4 2
h: forall x y : nat, P x y -> Q x
Q 4

  
P: nat -> nat -> Prop
Q: nat -> Prop
hP: P 4 2
h: forall x y : nat, P x y -> Q x
P 4 2
 assumption.
Qed.

forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
P 4 2 -> (forall x y : nat, P x y -> Q x) -> Q 4


forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
P 4 2 -> (forall x y : nat, P x y -> Q x) -> Q 4

  
P: nat -> nat -> Prop
Q: nat -> Prop
hP: P 4 2
h: forall x y : nat, P x y -> Q x
Q 4

  
P: nat -> nat -> Prop
Q: nat -> Prop
hP: P 4 2
h: forall x y : nat, P x y -> Q x
P 4 ?y

  eassumption.

Notice how we need the e here too!

Qed.

forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
P 4 2 -> (forall x y : nat, P x y -> Q x) -> Q 4


forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
P 4 2 -> (forall x y : nat, P x y -> Q x) -> Q 4

  eauto.
Qed.
Exercise: eauto

Solve the following goal.

forall (A : Type) (P : A -> A -> Prop) (Q : A -> Prop),
(forall x : A, exists y : A, P x y) ->
(forall x y : A, P x y -> Q x) -> forall x : A, Q x


forall (A : Type) (P : A -> A -> Prop) (Q : A -> Prop),
(forall x : A, exists y : A, P x y) ->
(forall x y : A, P x y -> Q x) -> forall x : A, Q x

Admitted.
Exercise: Logical equivalences (advanced)

Another interesting feature of Rocq is the ability to rewrite on other things rather than just equality.

For instance, we can use rewrite for logical equivalences. Let us go through it step by step.

To begin, prove the following logical equivalences.

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


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

Admitted.


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


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

Admitted.


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


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

Admitted.


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


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

Admitted.


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


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

Admitted.
Exercise: Rewriting with equivalences (advanced)

Now you can solve the following goals just by using rewrite on equivalences. No more need for split!

Note that you can also use reflexivity, symmetry and transitivity on those. Under the hood, this is using class resolution to find the proper instances. For iff (logical equivalence) they are already registered so we can freely use them.

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


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

Admitted.


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


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

Admitted.
Exercise: Set equality on lists (advanced)

Ok, this is getting old. We're going to switch to another relation which isn't already registered in the standard library. First we're going to introduce a relation on lists that relates two lists if they have the same elements (regardless of how many times they appear), i.e., if they represent the same set.

Complete the following definition.

Definition list_set_eq {A} (u v : list A) : Prop :=
  REPLACE_ME.

Notation "u ~ v" := (list_set_eq u v) (at level 70).

We first need to show that the relation is reflexive, symmetric and transitive. We do so by instantiating the right classes so that we can use the corresponding tactics (as for iff).

Check it works with the provided goal.

From Stdlib Require Import Setoid.


forall A : Type, Reflexive list_set_eq


forall A : Type, Reflexive list_set_eq

Admitted.


forall A : Type, Symmetric list_set_eq


forall A : Type, Symmetric list_set_eq

Admitted.


forall A : Type, Transitive list_set_eq


forall A : Type, Transitive list_set_eq

Admitted.


forall (A : Type) (u v w : list A), v ~ u -> (u ~ u -> v ~ w) -> u ~ w


forall (A : Type) (u v w : list A), v ~ u -> (u ~ u -> v ~ w) -> u ~ w

Admitted.
Exercise: Rewriting with set equality (advanced)

We will use the following command to register this relation to use with rewrite. Rocq will find the instances of equivalence relation we provided above. Otherwise we could provide them manually. Look up the documentation if you want to do that: https://rocq-prover.org/doc/master/refman/addendum/generalized-rewriting.html

On the left of the colon we give the list of parameters, here there is only one which is the type of values. We call it A and we can refer to it after the colon. The next argument is the type of elements we compare with the relation: list A. Then we give the relation itself: list_set_eq. Finally we give a name to the setoid relation. This is for Rocq's internal use.

Prove the following goal using rewrite. This is just transitivity again but this is to show you how it works on a simple example.

Add Parametric Relation A : (list A) list_set_eq as list_set_rel.


forall (A : Type) (u v w : list A), u ~ v -> v ~ w -> u ~ w


forall (A : Type) (u v w : list A), u ~ v -> v ~ w -> u ~ w

Admitted.

Prove that u ++ v ~ v ++ u.

forall (A : Type) (u v : list A), u ++ v ~ v ++ u


forall (A : Type) (u v : list A), u ++ v ~ v ++ u

Admitted.
Exercise: Morphisms (advanced)

In order to rewrite this relation inside, e.g., In, we have to first show that In is invariant under ~. In other words, that u ~ v implies In x u <-> In x v. We can use the following command to declare it. This will in turn let us rewrite inside In.

Prove that we indeed have a morphism. Prove the given goals using rewrite.

A: Type
x: A
forall x0 y : list A, x0 ~ y -> In x x0 <-> In x y


A: Type
x: A
forall x0 y : list A, x0 ~ y -> In x x0 <-> In x y

Admitted.


forall (A : Type) (x : A) (u v : list A), In x (u ++ v) -> In x (v ++ u)


forall (A : Type) (x : A) (u v : list A), In x (u ++ v) -> In x (v ++ u)

Admitted.


forall (A : Type) (x a b c : A) (u v : list A),
In x (u ++ [a; b; c] ++ x :: v)


forall (A : Type) (x a b c : A) (u v : list A),
In x (u ++ [a; b; c] ++ x :: v)

Admitted.

Look up the Forall predicate. Show that it is a morphism for list_set_eq. Proceed to solve the following goal.

forall u v w : list nat,
let P := fun n : nat => exists m : nat, n = 2 * m in
Forall P (w ++ u ++ v) -> Forall P (u ++ v ++ w)


forall u v w : list nat,
let P := fun n : nat => exists m : nat, n = 2 * m in
Forall P (w ++ u ++ v) -> Forall P (u ++ v ++ w)

Admitted.