(* Equations                                                          *)
(* Copyright (c) 2009-2021 Matthieu Sozeau <matthieu.sozeau@inria.fr> *)
(* This file is distributed under the terms of the                    *)
(* GNU Lesser General Public License Version 2.1                      *)

Basic examples

This file containts various examples demonstrating the features of Equations. If running this interactively you can ignore the printing and hide directives which are just used to instruct coqdoc.

Require Import Program Bvector List Relations.
From Equations Require Import Equations Signature.
Require Import Utf8.

Set Keyed Unification.

Just pattern-matching
Equations neg (b : bool) : bool :=
neg true := false ;
neg false := true.

A proof using the functional elimination principle derived for neg.
Lemma neg_inv : b, neg (neg b) = b.
Proof. intros b. funelim (neg b); auto. Qed.

Module Obligations.

One can use equations similarly to Program or the refine tactic, putting underscores _ for subgoals to be filled separately using the tactic mode.
  Equations? f (n : nat) : nat :=
  f 0 := 42 ;
  f (S m) with f m :=
    f (S m) IH := _
  Proof. intros. exact IH. Defined.

End Obligations.

Structural recursion and use of the with feature to look at the result of a recursive call (here with a trivial pattern-matching.

Import List.
Equations app_with {A} (l l' : list A) : list A :=
app_with nil l := l ;
app_with (cons a v) l with app_with v l ⇒ {
  | vl := cons a vl }.

Structurally recursive function on natural numbers, with inspection of a recursive call result. We use auto with arith to discharge the obligations.

Obligation Tactic := program_simpl ; try CoreTactics.solve_wf ; auto with arith.

Equations equal (n m : nat) : { n = m } + { n m } :=
equal O O := in_left ;
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 p) := in_right } ;
equal x y := in_right.

Pattern-matching on the indexed equality type.
Equations eq_sym {A} (x y : A) (H : x = y) : y = x :=
eq_sym x _ eq_refl := eq_refl.

Equations eq_trans {A} (x y z : A) (p : x = y) (q : y = z) : x = z :=
eq_trans x _ _ eq_refl eq_refl := eq_refl.

Notation vector := Vector.t.
Derive Signature for eq vector.

Module KAxiom.

By default we disallow the K axiom, but it can be set.
In this case the following definition fails as K is not derivable on type A.
  Fail Equations K {A} (x : A) (P : x = x Type) (p : P eq_refl) (H : x = x) : P H :=
    K x P p eq_refl := p.

  Set Equations With UIP.
  Axiom uip : A, UIP A.
  Local Existing Instance uip.
  Equations K_ax {A} (x : A) (P : x = x Type) (p : P eq_refl) (H : x = x) : P H :=
    K_ax x P p eq_refl := p.

The definition is however using an axiom equivalent to K, so it cannot reduce on closed or open terms.
End KAxiom.

Module KDec.
However, types enjoying a provable instance of the K principle are fine using the With UIP option. Note that the following definition does *not* reduce according to its single clause on open terms, it instead computes using the decidable equality proof on natural numbers.

  Set Equations With UIP.

  Fail Equations K {A} (x : A) (P : x = x Type) (p : P eq_refl) (H : x = x) : P H :=
    K x P p eq_refl := p.

  Equations K (x : nat) (P : x = x Type) (p : P eq_refl) (H : x = x) : P H :=
    K x P p eq_refl := p.
  Print Assumptions K. (* Closed under the global context *)

End KDec.

The with construct allows to pattern-match on an intermediary computation. The "|" syntax provides a shortcut to repeating the previous patterns.
Section FilterDef.
  Context {A} (p : A bool).

  Equations filter (l : list A) : list A :=
  filter nil := nil ;
  filter (cons a l) with p a ⇒ {
                       | true := a :: filter l ;
                       | false := filter l }.

By default, equations makes definitions opaque after definition, to avoid spurious unfoldings, but this can be reverted on a case by case basis, or using the global Set Equations Transparent option.
  Global Transparent filter.

End FilterDef.

We define inclusion of a list in another one, to specify the behavior of filter
Inductive incl {A} : relation (list A) :=
  stop : incl nil nil
| keep {x : A} {xs ys : list A} : incl xs ys incl (x :: xs) (x :: ys)
| {x : A} {xs ys : list A} : incl xs ys incl (xs) (x :: ys).

Using with again, we can produce a proof that the filtered list is a sublist of the original list.
Equations sublist {A} (p : A bool) (xs : list A) : incl (filter p xs) xs :=
sublist p nil := stop ;
sublist p (cons x xs) with p x := {
  | true := keep (sublist p xs) ;
  | false := skip (sublist p xs) }.

Well-founded definitions:

Require Import Arith Wf_nat.

One can declare new well-founded relations using instances of the WellFounded typeclass.
#[local] Instance wf_nat : WellFounded lt := lt_wf.
#[local] Hint Resolve lt_n_Sn : lt.

The by wf n lt annotation indicates the kind of well-founded recursion we want.
Equations testn (n : nat) : nat by wf n lt :=
testn 0 := 0 ;
testn (S n) with testn n ⇒ {
  | 0 := S 0 ;
  | (S n') := S n' }.

Notations for vectors
Equations Derive NoConfusion NoConfusionHom for vector.

Arguments Vector.nil {A}.
Arguments Vector.cons {A} _ {n}.

Declare Scope vect_scope.
Notation " x |:| y " := (@Vector.cons _ x _ y) (at level 20, right associativity) : vect_scope.
Notation " x |: n :| y " := (@Vector.cons _ x n y) (at level 20, right associativity) : vect_scope.
Notation "[]v" := Vector.nil (at level 0) : vect_scope.
Local Open Scope vect_scope.

We can define functions by structural recursion on indexed datatypes like vectors.

Equations vapp {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
  vapp []v w := w ;
  vapp (Vector.cons a v) w := a |:| vapp v w.

We can also support well-founded recursion on indexed datatypes.
We show that decidable equality of the elements type implied decidable equality of vectors.

#[local] Instance vector_eqdec {A n} `(EqDec A) : EqDec (vector A n).
Proof. intros. intros x. induction x. left. now depelim y.
  intro y; depelim y.
  destruct (eq_dec h h0); subst.
  destruct (IHx y). subst.
  left; reflexivity.
  right. intro. apply n0. noconf H0. constructor.
  right. intro. apply n0. noconf H0. constructor.
Print Assumptions vector_eqdec.

We automatically derive the signature and subterm relation for vectors and prove it's well-foundedness. The signature provides a signature_pack function to pack a vector with its index. The well-founded relation is defined on the packed vector type.

Derive Subterm for vector.

The relation is actually called t_subterm as vector is just a notation for Vector.t.

Section foo.
  Context {A B : Type}.

We can use the packed relation to do well-founded recursion on the vector. Note that we do a recursive call on a substerm of type vector A n which must be shown smaller than a vector A (S n). They are actually compared at the packed type { n : nat & vector A n}.

  Equations unzip {n} (v : vector (A × B) n) : vector A n × vector B n
    by wf (signature_pack v) (@t_subterm (A × B)) :=
  unzip []v := ([]v, []v) ;
  unzip (Vector.cons (x, y) v) with unzip v := {
    | pair xs ys := (Vector.cons x xs, Vector.cons y ys) }.
End foo.

Playing with lists and functional induction, we define a tail-recursive version of rev and show its equivalence with the "naïve" rev.

Equations app {A} (l l' : list A) : list A :=
app nil l := l;
app (cons a v) l := cons a (app v l).

Infix "++" := app (right associativity, at level 60) : list_scope.

Equations rev_acc {A} (l : list A) (acc : list A) : list A :=
rev_acc nil acc := acc;
rev_acc (cons a v) acc := rev_acc v (a :: acc).

Equations rev {A} (l : list A) : list A :=
rev nil := nil;
rev (cons a v) := rev v ++ (cons a nil).

Notation " [] " := List.nil.

Lemma app_nil : {A} (l : list A), l ++ [] = l.
  funelim (app l []); simpl. reflexivity.
  now rewrite H.

Lemma app_assoc : {A} (l l' l'' : list A), (l ++ l') ++ l'' = l ++ (l' ++ l'').
Proof. intros. revert l''.
  funelim (l ++ l'); intros; simp app; trivial.
  now rewrite H.

Lemma rev_rev_acc : {A} (l : list A), rev_acc l [] = rev l.
  replace (rev l) with (rev l ++ []) by apply app_nil.
  generalize (@nil A).
  funelim (rev l). reflexivity.
  intros l'. simp rev_acc; trivial. rewrite H.
  rewrite app_assoc. reflexivity.
#[local] Hint Rewrite @rev_rev_acc : rev_acc.
#[local] Hint Rewrite @app_nil @app_assoc : app.

Lemma rev_app : {A} (l l' : list A), rev (l ++ l') = rev l' ++ rev l.
Proof. intros. funelim (l ++ l'); simp rev app; trivial.
  now (rewrite H, <- app_assoc).

Equations zip' {A} (f : A A A) (l l' : list A) : list A :=
zip' f nil nil := nil ;
zip' f (cons a v) (cons b w) := cons (f a b) (zip' f v w) ;
zip' f x y := nil.

Equations zip'' {A} (f : A A A) (l l' : list A) (def : list A) : list A :=
zip'' f nil nil def := nil ;
zip'' f (cons a v) (cons b w) def := cons (f a b) (zip'' f v w def) ;
zip'' f nil (cons b w) def := def ;
zip'' f (cons a v) nil def := def.

Import Vector.


Equations vector_append_one {A n} (v : vector A n) (a : A) : vector A (S n) :=
vector_append_one nil a := cons a nil;
vector_append_one (cons a' v) a := cons a' (vector_append_one v a).

Equations vrev {A n} (v : vector A n) : vector A n :=
vrev nil := nil;
vrev (cons a v) := vector_append_one (vrev v) a.

Definition cast_vector {A n m} (v : vector A n) (H : n = m) : vector A m.
intros; subst; assumption. Defined.

Equations vrev_acc {A n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
vrev_acc nil w := w;
vrev_acc (cons a v) w := cast_vector (vrev_acc v (cons a w)) _.
(* About vapp'. *)

Record vect {A} := mkVect { vect_len : nat; vect_vector : vector A vect_len }.
Coercion mkVect : vector >-> vect.
Derive NoConfusion for vect.

Splitting a vector into two parts.

Inductive Split {X : Type}{m n : nat} : vector X (m + n) Type :=
  append : (xs : vector X m)(ys : vector X n), Split (vapp xs ys).

Arguments Split [ X ].

We split by well-founded recursion on the index m here.

Equations split {X : Type} {m n} (xs : vector X (m + n)) : Split m n xs by wf m :=
split (m:=O) xs := append nil xs ;
split (m:=S m) (cons x xs) with split xs ⇒ {
  | append xs' ys' := append (cons x xs') ys' }.

The split and vapp functions are inverses.

Lemma split_vapp : (X : Type) m n (v : vector X m) (w : vector X n),
  let 'append v' w' := split (vapp v w) in
    v = v' w = w'.
  funelim (vapp v w).
  destruct split. depelim xs; intuition.
  simp split in ×. destruct split. simpl.
  intuition congruence.

(* Eval compute in @zip''. *)

Require Import Bvector.

This function can also be defined by structural recursion on m.

Equations split_struct {X : Type} {m n} (xs : vector X (m + n)) : Split m n xs :=
split_struct (m:=0) xs := append nil xs ;
split_struct (m:=(S m)) (cons x xs) with split_struct xs ⇒ {
  split_struct (m:=(S m)) (cons x xs) (append xs' ys') := append (cons x xs') ys' }.

Lemma split_struct_vapp : (X : Type) m n (v : vector X m) (w : vector X n),
  let 'append v' w' := split_struct (vapp v w) in
    v = v' w = w'.
  intros. funelim (vapp v w); simp split_struct in ×.
  destruct split_struct. depelim xs; intuition.
  destruct (split_struct (vapp v _)); simpl.
  intuition congruence.

Taking the head of a non-empty vector.

Equations vhead {A n} (v : vector A (S n)) : A :=
vhead (cons a v) := a.

Mapping over a vector.

Equations vmap' {A B} (f : A B) {n} (v : vector A n) : vector B n :=
vmap' f nil := nil ;
vmap' f (cons a v) := cons (f a) (vmap' f v).
#[local] Hint Resolve lt_n_Sn : subterm_relation.
Transparent vmap'.

The same, using well-founded recursion on n.
Equations vmap {A B} (f : A B) {n} (v : vector A n) : vector B n by wf n :=
vmap f (n:=?(O)) nil := nil ;
vmap f (cons a v) := cons (f a) (vmap f v).

Transparent vmap.
Eval compute in (vmap' id (@nil nat)).
Eval compute in (vmap' id (@cons nat 2 _ nil)).

The image of a function.

Section Image.
  Context {S T : Type}.
  Variable f : S T.

  Inductive Imf : T Type := imf (s : S) : Imf (f s).

Here (f s) is innaccessible.

  Equations inv (t : T) (im : Imf t) : S :=
  inv ?(f s) (imf s) := s.

End Image.

Working with a universe of types with an interpretation function.

Section Univ.

  Inductive univ : Set :=
  | ubool | unat | uarrow (from:univ) (to:univ).

  Equations interp (u : univ) : Set :=
  interp ubool := bool; interp unat := nat;
  interp (uarrow from to) := interp from interp to.

  Transparent interp.

  Definition interp' := Eval compute in @interp.

  Equations foo (u : univ) (el : interp' u) : interp' u :=
  foo ubool true := false ;
  foo ubool false := true ;
  foo unat t := t ;
  foo (uarrow from to) f := id f.

  Transparent foo.
  (* Eval lazy beta delta  foo foo_obligation_1 foo_obligation_2  iota zeta in foo. *)

End Univ.

Equations vlast {A} {n} (v : vector A (S n)) : A by struct v :=
vlast (@cons a O _) := a ;
vlast (@cons a (S n) v) := vlast v.
Transparent vlast.

The parity predicate embeds a divisor of n or n-1

Inductive Parity : nat Set :=
| even : n, Parity (mult 2 n)
| odd : n, Parity (S (mult 2 n)).

(* Eval compute in (fun n => mult 2 (S n)). *)
Definition cast {A B : Type} (a : A) (p : A = B) : B.
  intros. subst. exact a.

Equations parity (n : nat) : Parity n :=
parity O := even 0 ;
parity (S n) with parity n ⇒ {
  parity (S ?(mult 2 k)) (even k) := odd k ;
  parity (S ?(S (mult 2 k))) (odd k) := cast (even (S k)) _ }.

We can halve a natural looking at its parity and using the lower truncation.

Equations half (n : nat) : nat :=
half n with parity n ⇒ {
  half ?(S (mult 2 k)) (odd k) := k ;
  half ?(mult 2 k) (even k) := k }.

Equations vtail {A n} (v : vector A (S n)) : vector A n :=
  vtail (cons a v') := v'.

Equations diag {A n} (v : vector (vector A n) n) : vector A n :=
diag (n:=O) nil := nil ;
diag (n:=S ?(n)) (cons (@cons a n v) v') := cons a (diag (vmap vtail v')).
Transparent diag.

Definition mat A n m := vector (vector A m) n.

Equations vmake {A} (n : nat) (a : A) : vector A n :=
vmake O a := nil ;
vmake (S n) a := cons a (vmake n a).

Equations vfold_right {A : nat Type} {B} (f : n, B A n A (S n)) (e : A 0) {n} (v : vector B n) : A n :=
vfold_right f e nil := e ;
vfold_right f e (@cons a n v) := f n a (vfold_right f e v).

Equations vzip {A B C n} (f : A B C) (v : vector A n) (w : vector B n) : vector C n :=
vzip f nil _ := nil ;
vzip f (cons a v) (cons a' v') := cons (f a a') (vzip f v v').

Definition transpose {A m n} : mat A m n mat A n m :=
  vfold_right (A:=λ m, mat A n m)
  (λ m', vzip (λ a, cons a))
  (vmake n nil).

Require Import Examples.Fin.

Generalizable All Variables.

Opaque vmap. Opaque vtail. Opaque nth.

Lemma nth_vmap `(v : vector A n) `(fn : A B) (f : fin n) : nth (vmap fn v) f = fn (nth v f).
Proof. revert B fn. funelim (nth v f); intros; now simp nth vmap. Qed.

Lemma nth_vtail `(v : vector A (S n)) (f : fin n) : nth (vtail v) f = nth v (fs f).
Proof. funelim (vtail v); intros; now simp nth. Qed.

#[local] Hint Rewrite @nth_vmap @nth_vtail : nth.

Lemma diag_nth `(v : vector (vector A n) n) (f : fin n) : nth (diag v) f = nth (nth v f) f.
Proof. revert f. funelim (diag v); intros f.
  depelim f.

  depelim f; simp nth; trivial.
  rewrite H. now simp nth.

Equations assoc (x y z : nat) : x + y + z = x + (y + z) :=
assoc 0 y z := eq_refl;
assoc (S x) y z with assoc x y z, x + (y + z) ⇒ {
assoc (S x) y z eq_refl _ := eq_refl }.

Section well_founded_recursion_and_auxiliary_function.

When recursive calls are made on results pattern-matching the output of auxiliary functions, you need enough information to prove that the argument of recursive calls are smaller. This is usually granted by the specification of the auxiliary function (see function pivot in the quicksort example). When the type of the recursive function is not informative enough, we can use an inspect pattern as illustrated in the following example.

Context {A : Type} (f : A option A) {lt : A A Prop}
 `{WellFounded A lt}.

Hypothesis decr_f : n p, f n = Some p lt p n.

The inspect definition is used to pack a value with a proof of an equality to itself. When pattern matching on the first component in this existential type, we keep information about the origin of the pattern available in the second component, the equality.
Definition inspect {A} (a : A) : {b | a = b} :=
  exist _ a eq_refl.

Notation "x 'eqn:' p" := (exist _ x p) (only parsing, at level 20).

If one uses f n instead of inspect (f n) in the following definition, patterns should be patterns for the option type, but then there is an unprovable obligation that is generated as we don't keep information about the call to f n being equal to Some p to justify the recursive call to f_sequence.
Equations f_sequence (n : A) : list A by wf n lt :=
  f_sequence n with inspect (f n) := {
    | Some p eqn: eq1p :: f_sequence p;
    | None eqn:_List.nil

The following is an illustration of a theorem on f_sequence.
Lemma in_seq_image (n p : A) : List.In p (f_sequence n)
    k, f k = Some p.
funelim (f_sequence n);[ | now intros abs; elim abs].
now simpl; intros [p_is_a | p_in_seq];[rewrite <- p_is_a; n | auto].

End well_founded_recursion_and_auxiliary_function.

Module IdElim.
Import Sigma_Notations.
Set Equations Transparent.
Equations transport {A : Type} (P : A Type) {x y : A} (p : x = y) (u : P x) : P y :=
transport P eq_refl u := u.

Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing).

Equations path_sigma {A : Type} {P : A Type} (u v : sigma P)
  (p : u.1 = v.1) (q : p # u.2 = v.2) : u = v :=
path_sigma (_ , _) (_ , _) eq_refl eq_refl := eq_refl.

Example foo := path_sigma_elim.
End IdElim.

This page has been generated by coqdoc