MPRI PRFA — Proof Assistants

Records

From Coq Require Import Lia List ZArith.
Import ListNotations.

In Coq you can write structures using what we call "records". They consists 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
}.
bad_rational1 is defined
numerator is defined
denominator is defined

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

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

Arguments Build_bad_rational1 (numerator denominator)%nat_scopeArguments numerator bArguments denominator b
About Build_bad_rational1.
Build_bad_rational1 : nat -> nat -> bad_rational1Build_bad_rational1 is not universe polymorphicArguments Build_bad_rational1 (numerator denominator)%nat_scopeExpands to: Constructor lesson4.Build_bad_rational1Declared in toplevel input, characters 70-83

We can produce values as follows:

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

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

Compute (numerator half).
= 1
: nat
Compute (denominator half).
= 2
: nat

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

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

NOTE: To write integers in Z, we can use numeral notations as long as we add %Z at the end to indicate that we don't mean a nat.

Definition half' := {|
  numerator' := 1%Z ;
  denominator' := 2
|}.
half' is defined

We can also produce values interactively.

Definition quarter : bad_rational2.
bad_rational2
Proof.
bad_rational2

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

  constructor.
Z
nat
  -
Z exact 1%Z.
  -
nat exact 4.
Defined.
quarter is defined

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

About Build_rational.
Build_rational : Z -> forall denominator'' : nat, denominator'' <> 0 -> rationalBuild_rational is not universe polymorphicArguments Build_rational numerator''%Z_scope denominator''%nat_scope den_not_zeroExpands to: Constructor lesson4.Build_rationalDeclared in toplevel input, characters 540-548

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

We can also produce values interactively.

Definition quarter'' : rational.
rational
Proof.
rational
  refine (Build_rational _ _ _).
Z
?Goal0 <> 0

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

Abort.
Definition quarter'' : rational.
rational

the tactic constructor fails because it cannot introduce evars

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

econstructor can

  econstructor.
Z
?denominator'' <> 0
Abort.
Definition quarter'' : rational.
rational

same for apply:

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

eapply works

  eapply Build_rational.
Z
?denominator'' <> 0
  -
Z exact 1%Z.
  -
?denominator'' <> 0 assert (4 <> 0) as H by lia.
H: 4 <> 0
?denominator'' <> 0
    exact H.
Abort.
Definition quarter'' : rational.
rational
   eapply (Build_rational 1).
?denominator'' <> 0
   instantiate (1 := 4).
4 <> 0 lia.
Abort.
Definition quarter'' : rational.
rational
  refine {| numerator'' := 1 ; denominator'' := 4 |}.
4 <> 0
  lia.
Defined.
quarter'' is defined

Actually products that are defined using an inductive type, can also be defined as records. For this we use parame ters 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
}.
prod' is defined
fst' is defined
snd' is defined

Definition some_pair := mkpair _ _ 12 bool.
some_pair is defined
Print some_pair.
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.
some_other_pair is defined

You can also use 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.
to_prod is defined

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).
to_prod_alt is defined

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).
to_prod_alt2 is defined

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).
to_prod_alt3 is defined

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)
}.
monoid is defined
m_ty is defined
m_ne is defined
m_op is defined
m_l_ne is defined
m_r_ne is defined
m_assoc is defined

Again we can build these structures interactively using refine.

Definition nat_monoid : monoid.
monoid
Proof.
monoid
  refine {|
    m_ty := nat ;
    m_ne := 0 ;
    m_op n m := n + m
  |}.
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 intro.
x: nat
0 + x = x reflexivity.
  -
forall x : nat, x + 0 = x intro.
x: nat
x + 0 = x rewrite <- plus_n_O.
x: nat
x = x reflexivity.
  -
forall x y z : nat, x + y + z = x + (y + z) intros x y z.
x, y, z: nat
x + y + z = x + (y + z) rewrite Nat.add_assoc.
x, y, z: nat
x + y + z = x + y + z reflexivity.
Defined.
nat_monoid is defined 

We need Defined to access the fields!

Compute nat_monoid.(m_ne).
= 0
: m_ty nat_monoid 

Notation for m_neu nat_monoid

Check nat_monoid.(m_op).
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).

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

Lemma monoid_fact :
  forall (M : monoid) (x y : M.(m_ty)),
    x ** M.(m_ne) ** y = x ** y.
forall (M : monoid) (x y : m_ty M), x ** m_ne M ** y = x ** y
Proof.
forall (M : monoid) (x y : m_ty M), x ** m_ne M ** y = x ** y
  intros M x y.
M: monoid
x, y: m_ty M
x ** m_ne M ** y = x ** y

More complicated than necessary of course

  rewrite m_assoc.
M: monoid
x, y: m_ty M
x ** (m_ne M ** y) = x ** y rewrite m_l_ne.
M: monoid
x, y: m_ty M
x ** y = x ** y reflexivity.
Qed.
monoid_fact is defined

Lemma nat_fact :
  forall (x y : nat),
    x + 0 + y = x + y.
forall x y : nat, x + 0 + y = x + y
Proof.
forall x y : nat, x + 0 + y = x + y
  intros x y.
x, y: nat
x + 0 + y = x + y
  apply monoid_fact with (M := nat_monoid).
Qed.
nat_fact is defined

Products of monoids also yields a monoid.

Definition prod_monoid (M1 M2 : monoid) : monoid.
M1, M2: monoid
monoid
Proof.
M1, M2: monoid
monoid
  refine {|
    m_ty := M1.(m_ty) * M2.(m_ty) ;
    m_ne := (M1.(m_ne), M2.(m_ne)) ;
    m_op '(x,y) '(u,v) := (x ** u, y ** v)
  |}.
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 intros [x y].
M1, M2: monoid
x: m_ty M1
y: m_ty M2
(m_ne M1 ** x, m_ne M2 ** y) = (x, y) rewrite !m_l_ne.
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 intros [x y].
M1, M2: monoid
x: m_ty M1
y: m_ty M2
(x ** m_ne M1, y ** m_ne M2) = (x, y) rewrite !m_r_ne.
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) intros [x y] [u v] [a 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)) rewrite !m_assoc.
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.
prod_monoid is defined

Type class

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

Check monoid_fact (prod_monoid nat_monoid nat_monoid).
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 Coq can't find the monoid structure on its own.

Fail Lemma nat_nat_fact :
  forall (a b c d : nat),
    (a, b) ** (0, 0) ** (c, d) = (a, b) ** (c, d).
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".

Lemma nat_nat_fact :
  forall (a b c d : nat),
    ((prod_monoid nat_monoid nat_monoid).(m_op) (a, b) (0, 0)) ** (c, d) =
    (prod_monoid nat_monoid nat_monoid).(m_op) (a, b) (c, d).
forall a b c d : nat, (a, b) ** (0, 0) ** (c, d) = (a, b) ** (c, d)
Proof.
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!

  intros a b c d.
a, b, c, d: nat
(a, b) ** (0, 0) ** (c, d) = (a, b) ** (c, d)
  apply monoid_fact.
Qed.
nat_nat_fact is defined

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 Coq. We move the carrier, neutral and operation as parameters because Coq 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)
}.
Monoid is defined
mon_left_neutral is defined
mon_right_neutral is defined
mon_assoc is defined

Instance is a a special command for definitions that register them as things Coq 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.

#[export] Instance MonoidNat : Monoid nat 0 plus.
Monoid nat 0 Init.Nat.add
Proof.
Monoid nat 0 Init.Nat.add
  split.
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 intro.
x: nat
0 + x = x reflexivity.
  -
forall x : nat, x + 0 = x intro.
x: nat
x + 0 = x lia.
  -
forall x y z : nat, x + y + z = x + (y + z) intros.
x, y, z: nat
x + y + z = x + (y + z) lia.
Qed.
MonoidNat is defined

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

Lemma test_nat :
  forall k n m, k + n + m + 0 = k + (n + m).
forall k n m : nat, k + n + m + 0 = k + (n + m)
Proof.
forall k n m : nat, k + n + m + 0 = k + (n + m)
  intros.
k, n, m: nat
k + n + m + 0 = k + (n + m)
  rewrite mon_right_neutral.
k, n, m: nat
k + n + m = k + (n + m)
  rewrite mon_assoc.
k, n, m: nat
k + (n + m) = k + (n + m) reflexivity.
Qed.
test_nat is defined

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

Lemma test_monoid :
  forall M neu op `{Monoid M neu op} k n 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)
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)
  intros.
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)
  rewrite mon_right_neutral.
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)
  rewrite mon_assoc.
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.
test_monoid is defined

Lemma test_nat' :
  forall k n m, k + n + m + 0 = k + (n + m).
forall k n m : nat, k + n + m + 0 = k + (n + m)
Proof.
forall k n m : nat, k + n + m + 0 = k + (n + m)
  intros.
k, n, m: nat
k + n + m + 0 = k + (n + m) apply test_monoid.
k, n, m: nat
Monoid nat 0 Init.Nat.add

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

  exact _.
Qed.
test_nat' is defined

EXERCISE

Complete the product instance.

#[export] Instance MonoidProd :
  forall A B na nb opa opb,
    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))
Proof.
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.
MonoidProd is declared

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

Definition foo : Monoid (nat * nat * nat) _ _ := _.
foo is defined
Print foo.
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))

Here is another example of class: decidable equality.

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

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, Coq 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.
memb is defined
memb is recursively defined (guarded on 4th argument)

Search (nat -> nat -> bool).
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.

#[export, refine] Instance Eq_nat : Eq nat := {|
  eqb := Nat.eqb
|}.
forall x y : nat, (x =? y) = true <-> x = y
Proof.
forall x y : nat, (x =? y) = true <-> x = y
  Search Nat.eqb.
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.
Eq_nat is defined 

We still need to use Defined though.

Compute (eqb 0 1).
= false
: bool
Compute (eqb 12 12).
= true
: bool

Compute (memb 1 [ 3 ; 5 ; 1 ]).
= true
: bool
Compute (memb 12 [ 3 ; 5 ; 1 ]).
= false
: bool

Automation

Classes are one form of automation. There are others in Coq. 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.

Lemma In_hd :
  forall A (x : A) l,
    In x (x :: l).
forall (A : Type) (x : A) (l : list A), In x (x :: l)
Proof.
forall (A : Type) (x : A) (l : list A), In x (x :: l)
  intros A x l.
A: Type
x: A
l: list A
In x (x :: l)
  simpl.
A: Type
x: A
l: list A
x = x \/ In x l left.
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.
Lemma In_hd :
  forall A (x : A) l,
    In x (x :: l).
forall (A : Type) (x : A) (l : list A), In x (x :: l)
Proof.
forall (A : Type) (x : A) (l : list A), In x (x :: l)
  intros A x l.
A: Type
x: A
l: list A
In x (x :: l)
  simpl.
A: Type
x: A
l: list A
x = x \/ In x l auto.
Qed.
In_hd is defined

Lemma In_tl :
  forall A (x y : A) l,
    In x l ->
    In x (y :: l).
forall (A : Type) (x y : A) (l : list A), In x l -> In x (y :: l)
Proof.
forall (A : Type) (x y : A) (l : list A), In x l -> In x (y :: l)
  intros A x y l h.
A: Type
x, y: A
l: list A
h: In x l
In x (y :: l)
  simpl.
A: Type
x, y: A
l: list A
h: In x l
y = x \/ In x l auto.
Qed.
In_tl is defined

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.

Lemma In_4 :
  forall A (x a b c d : A) l,
    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)
Proof.
forall (A : Type) (x a b c d : A) (l : list A), In x l -> In x (a :: b :: c :: d :: l)
  intros A x a b c d l h.
A: Type
x, a, b, c, d: A
l: list A
h: In x l
In x (a :: b :: c :: d :: l)
  auto.
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.

  apply In_tl.
A: Type
x, a, b, c, d: A
l: list A
h: In x l
In x (b :: c :: d :: l) apply In_tl.
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:

  repeat apply In_tl.
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.

Lemma In_hd' :
  forall A (x : A) l,
    In x (x :: l).
forall (A : Type) (x : A) (l : list A), In x (x :: l)
Proof.
forall (A : Type) (x : A) (l : list A), In x (x :: l)
  intros A x l.
A: Type
x: A
l: list A
In x (x :: l)
  auto.
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 Coq automatically uses core, but this behaviour is deprecated and will be removed. Instead, one should do so explicitly:

#[export] Hint Resolve In_hd : core.

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 disjointness and difference of constructors.

• tauto

For propositional logic. Solves (intuituinistic) propositional tautologies

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

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

Goal forall p, p \/ ~ p.
forall p : Prop, p \/ ~ p
Proof.
forall p : Prop, p \/ ~ p
  intros.
p: Prop
p \/ ~ p Fail tauto.
The command has indeed failed with message:
Tactic failure: tauto failed.
p: Prop
p \/ ~ p apply DNE.
p: Prop
~ ~ (p \/ ~ p) tauto.
Defined.
Unnamed_thm is defined

Or without manual work

Require Import Classical.

Goal forall p, p \/ ~ p.
forall p : Prop, p \/ ~ p
Proof.
forall p : Prop, p \/ ~ p
  intros.
p: Prop
p \/ ~ p tauto.
Defined.
Unnamed_thm0 is defined

• intuition / firstorder

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

• Existential variables, again

Goal forall n, n = 0 \/ exists m, n = S m.
forall n : nat, n = 0 \/ (exists m : nat, n = S m)
Proof.
forall n : nat, n = 0 \/ (exists m : nat, n = S m)
  intro n.
n: nat
n = 0 \/ (exists m : nat, n = S m)
  destruct n.
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) right.
n: nat
exists m : nat, S n = S m eexists.
n: nat
S n = S ?m reflexivity.

We're going to show the proof to see what auto picked for a value

  Show Proof.
(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.
Unnamed_thm1 is defined

auto also has an eauto variant. You can use it to deal with existential quantifiers. It is generally slower than auto so you can use it when auto fails.

Goal forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
  P 4 2 ->
  (forall x y, 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
Proof.
forall (P : nat -> nat -> Prop) (Q : nat -> Prop), P 4 2 -> (forall x y : nat, P x y -> Q x) -> Q 4
  intros P Q hP h.
P: nat -> nat -> Prop
Q: nat -> Prop
hP: P 4 2
h:= forall x y: nat, P x y -> Q x
Q 4
  apply h with (y := 2).
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.
Unnamed_thm2 is defined
Goal forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
    P 4 2 ->
    (forall x y, 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
Proof.
forall (P : nat -> nat -> Prop) (Q : nat -> Prop), P 4 2 -> (forall x y : nat, P x y -> Q x) -> Q 4
  intros P Q hP h.
P: nat -> nat -> Prop
Q: nat -> Prop
hP: P 4 2
h:= forall x y: nat, P x y -> Q x
Q 4
  eapply h.
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.
Unnamed_thm3 is defined
Goal forall (P : nat -> nat -> Prop) (Q : nat -> Prop),
    P 4 2 ->
    (forall x y, 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
Proof.
forall (P : nat -> nat -> Prop) (Q : nat -> Prop), P 4 2 -> (forall x y : nat, P x y -> Q x) -> Q 4
  eauto.
Qed.
Unnamed_thm4 is defined