Equations (Coq)

Declarations consist of

An inductive graph will be generated (by default. Can be changed).

For example, here:

From Equations Require Import Equations.

Equations neg (b : bool) : bool :=
neg true := false;
neg false := true.

(* Equations generate this automatically *)
Print neg_graph.
(*
Inductive neg_graph : bool -> bool -> Set :=
    neg_graph_equation_1 : neg_graph true false
  | neg_graph_equation_2 : neg_graph false true.

Arguments neg_graph (b _)%bool_scope
*)

—

Signature pack a value with its index. —

Dependent types are also useful to turn partial functions into total functions by restricting their domain.

General

Transparency/opacity

Empty pattern

! is the empty pattern in Equations

Note: When writing { |!}, make sure there is a space after {. Otherwise it's syntax of a Coq record.

An example:

Equations hd {A: Type} (l: list A) (pf: l <> []): A :=
hd [] pf with pf eq_refl := { |!};
hd (a::l) _ := a.

Have not yet figured out how pf eq_refl is appropriate here.

Holes

We can leave holes in the definition if needed. Each hole would generate a proof obligation. If Coq cannot resolve the obligations, we need to fulfill them. It would like in Program-Next Obligation.

—

An example where Coq can figure out all obligations by itself:

Equations equal (n m: nat): {n=m} + {n<>m} :=
equal O O := left eq_refl;
equal (S n) (S m) with equal n m := {
  equal (S n) (S ?(n)) (left eq_refl) := left eq_refl;
  equal (S n) (S m) (right _) := right _;
};
equal n m := right _.

?(n)

Syntax to allow for unification.

Equations eqt' {A: Type} (x y z: A) (pf1: x=y) (pf2: y=z): x=z :=
eqt' x ?(x) ?(x) eq_refl eq_refl := eq_refl.

Here the two ?(x)-s gets values from y and z, and are unified with the value of x.

From the manual:

The ?(x) notation is essentially denoting that the pattern is not a candidate for refinement, as it is determined by another pattern. This particular patterns are called "inaccessible". When they are variables the inaccessibility annotation is optional.

–

Although this particular example could also have been just:

Equations eqt {A: Type} {x y z: A} (pf1: x=y) (pf2: y=z): x=z :=
eqt eq_refl eq_refl := eq_refl.

with

An example:

Equations unzip {A: Type} (l: list (A * A)): list A * list A :=
unzip [] := ([], []);
unzip (x :: l) with unzip l => {
  unzip ((a,b)::l) (la, lb) := (a::la, b::lb)}.

Vectors

From Equations Require Import Equations.

Require Import Vector.
Import VectorNotations.

Arguments Vector.nil {A}.
Arguments Vector.cons {A} a {n} v: rename.

Equations vtail {A: Type} {n: nat}
  (v: Vector.t A (S n))
  : Vector.t A n :=
vtail (x::v) := v.

We didn't have to mention the case of empty vector because it was able to infer it.

Recursion

Following example to find diagonal vector a square matrix won't go through because Coq cannot see which argument is getting smaller:

(* Diagonal of a square matrix *)
Fail Equations diag {A: Type} {n: nat}
  (v: Vector.t (Vector.t A n) n)
  : Vector.t A n :=
diag [] := [];
diag ((x::v) :: v') := 
  x :: (diag (vmap vtail v')).
(*
The command has indeed failed with message:
Cannot guess decreasing argument of fix.
*)

But if we use n explicitly, somehow Equations help Coq figure it out (unification is involved??):

Equations diag {A: Type} {n: nat}
  (v: Vector.t (Vector.t A n) n)
  : Vector.t A n :=
diag (n:=O) [] := [];
diag (n:=S _) ((x::v) :: v') := 
  x :: (diag (vmap vtail v')).

Making primitive recursion explicit

Make well-foundedness explicit with wf.

Instead of letting coq's default way to figure out decreasing argument in a recursive definition.

wf allows Coq to have something more than just syntactic check to figure out decreasing argument in the definition.

Example (just for illustrative purposes. wf is not needed here):

Equations id' (n: nat): nat by wf n lt :=
id' O := O;
id' (S n') := id n'.

This says that successive values of n are related by the relation lt.

Obligations are automatically inserted to show that lt next curr holds all the way till the base case.

In this example, Coq can solve all obligations (n' < S n') automatically.

If the relation is heterogenous (ie, relates values of two different types, like (x: Vector.t A n) < (y: Vector.t A (S n)), obligations would be less simple.

Derive command of Equations can be used to generate types that can help provide structure in such cases.

Derive NoConfusion for Vector.t.
(* NoConfusionPackage_t is defined *)

Derive Subterm for Vector.t.
(*
t_direct_subterm is defined

t_direct_subterm_ind is defined

t_direct_subterm_sind is defined

t_direct_subterm_sig is defined

t_direct_subterm_sig_pack is defined

t_direct_subterm_Signature is defined

t_subterm is defined
*)

From Equations Require Import Equations.

Derive NoConfusion for sort.
Derive Signature NoConfusion NoConfusionHom for t.
Derive Subterm for t.

Check well_founded_t_subterm : forall A, WellFounded (t_subterm A).

(*   by wf (signature_pack f) (@t_subterm f) := *)

Attributes

Note: eliminator=yes implicitly sets equations=yes

Example:

#[derive(eliminator=no),
  tactic=simpl]
Equations hd {A: Type} (l: list A) (pf: l <> []): A :=
hd [] pf with pf eq_refl := { |!};
hd (a::l) _ := a.

Tactics

Errors

'cannot find covering'

Try Set Equations Debug. and see.

Will show where it went off track.

Settings

Misc

Leibniz substitution principle

A: Type
P: A -> Type
x, y: A
P x: Type
x = y: Prop
-----------------
P y: Type

Essentially says that given a P x, if x=y, then we can get a P y.