Coq demos of CoInductive, Setoid, Function

demos.v

(* Examples of co-induction, quotient types (setoid), custom termination *)

Require Import Coq.Init.Nat.
Require Import Coq.Unicode.Utf8.
Require Import Coq.Arith.Mult.
Require Import Coq.Arith.Compare_dec.
Require Import Coq.Classes.RelationClasses.
Require Import Coq.Classes.Morphisms.
Require Import Coq.micromega.Lia.
Import PeanoNat.Nat.

(*
CoInductive
-----------
A demo of proving stream equality
*)

Section ListStream.

Inductive list :=
  | nil : list
  | cons : nat -> list -> list.

CoInductive stream :=
  | prep : nat -> stream -> stream.

(* We can use pattern matching like as before. *)

Definition head l default :=
  match l with
  | nil => default
  | cons hd tl => hd
  end.

Definition hd s := match s with prep hd tl => hd end.
Definition tl s := match s with prep hd tl => tl end.

(* We can create infinite recursive structures. *)

Fail Fixpoint constant n := cons n (constant n).
CoFixpoint constant n := prep n (constant n).

(* We can define zip, even, odd like we saw with coalgebra. *)

CoFixpoint zip α β :=
  match α with
  | prep α0 α' => prep α0 (zip β α')
  end.

CoFixpoint even α :=
  match α with
  | prep α0 α' => prep α0 (even (tl α'))
  end.

Definition odd α := even (tl α).

(* Lets read some elements off the stream. *)

Fixpoint read α n :=
  match n with
  | 0 => nil
  | S m =>
    match α with
    | prep α0 α' => cons α0 (read α' m)
    end
  end.

(* Eval lazy in read (zip (constant 0) (constant 1)) 10. *)

(* To prove equality we need a new equality type. *)

Reserved Notation "α ~= β" (at level 90).
CoInductive s_eq : stream -> stream -> Prop :=
  | stream_eq h α β : α ~= β -> prep h α ~= prep h β
where "α ~= β" := (s_eq α β).

(* A proof of s_eq is a co-fixpoint. To help with this we use a bisimulation. *)
Section Bisimulation.
Variable R : stream -> stream -> Prop.

Hypothesis bisim1 : ∀ α β, R α β -> hd α = hd β.
Hypothesis bisim2 : ∀ α β, R α β -> R (tl α) (tl β).

Theorem bisimulation α β :
  R α β -> α ~= β.
Proof.
revert α β; cofix self.
destruct α, β; intro.
apply bisim1 in H as H1; apply bisim2 in H as H2.
simpl in *; subst n0.
constructor. now apply self.
Qed.

End Bisimulation.

Lemma zip_even_odd α :
  zip (even α) (odd α) ~= α.
Proof.
pose(R α β :=
  α = zip (even β) (odd β) \/
  ∃γ, α = zip (odd γ) (even (tl (tl γ))) /\ β = tl γ).
apply (bisimulation R).
- intros a b [H|[γ [H1 H2]]]; subst.
  now destruct b, b. now destruct γ, γ, γ.
- intros a b [H|[γ [H1 H2]]]; subst.
  + right; exists b; split. now destruct b. easy.
  + left. now destruct γ, γ.
- now left.
Qed.

End ListStream.

(*
Quotient types
--------------
A demo of rewriting using Setoid
*)

Definition modulo n a b := ∃m, a + m*n = b \/ b + m*n = a.
Definition mod8 := modulo 8.
Notation "a '≡8' b" := (mod8 a b) (at level 70).

Instance mod8_equivalence :
  Equivalence mod8.
Proof.
split.
- exists 0. lia.
- intros x y [m H]. exists m. lia.
- intros x y z [m [Hm|Hm]] [k [Hk|Hk]].
  + exists (m + k). lia.
  + destruct (le_dec m k). exists (k - m). lia. exists (m - k). lia.
  + destruct (le_dec m k). exists (k - m). lia. exists (m - k). lia.
  + exists (m + k). lia.
Qed.

Instance add_mod8_proper :
  Proper (mod8 ==> mod8 ==> mod8) add.
Proof.
intros m n [k [Hmn|Hmn]] x y [l [Hxy|Hxy]].
- exists (k + l). lia.
- destruct (le_dec k l). exists (l - k). lia. exists (k - l). lia.
- destruct (le_dec k l). exists (l - k). lia. exists (k - l). lia.
- exists (k + l). lia.
Qed.

Instance mul_mod8_proper :
  Proper (mod8 ==> mod8 ==> mod8) mul.
Proof.
intros m n [k [Hmn|Hmn]] x y [l [Hxy|Hxy]].
- exists (m*l + x*k + k*l*8). lia.
- destruct (le_dec (k*y) (m*l)).
  exists (m*l - k*y). lia. exists (k*y - m*l). lia.
- destruct (le_dec (k*y) (m*l)).
  exists (m*l - k*y). lia. exists (k*y - m*l). lia.
- exists (n*l + y*k + k*l*8). lia.
Qed.

Lemma example x y :
  x*7 ≡8 3*y -> 21*x+16 ≡8 9*y.
Proof.
intros H. replace (21*x) with (3*(x*7)) by lia.
rewrite H. replace (3*(3*y)) with (9*y) by lia.
assert (R: 16 ≡8 0). exists 2. lia.
rewrite R, plus_0_r.
reflexivity.
Qed.

(*
Custom termination
------------------
A demo of a custom termination proof using the Function (FunInd) extension
*)

Require Import FunInd.
Require Import Recdef.

Fail Fixpoint addition (m n : nat) :=
  if n =? 0 then m else addition (m + 1) (n - 1).

Function addition (m n : nat) {measure id n} :=
  if n =? 0 then m else addition (m + 1) (n - 1).
Proof.
intros. apply eqb_neq in teq. unfold id. lia.
Defined.

Eval lazy in (addition 8 7).

Lemma addition_spec m n :
  addition m n = m + n.
Proof.
apply addition_ind; intros.
apply eqb_eq in e; now subst.
rewrite H. apply eqb_neq in e. lia.
Qed.