lazy naturals

lazynat_semiring.v

Require Import
  interfaces.canonical_names
  interfaces.abstract_algebra.

(* Lazy evaluating trick. Coq is strict but a lambda term
   is not further evaluated. This allows you to trick Coq
   into lazy evaluation, like so: *)

Inductive lazy_nat : Type :=
  | lazy_O : lazy_nat
  | lazy_S : (unit -> lazy_nat) -> lazy_nat.

(*
Fixpoint lazy_mult n m :=
  match n with
  | lazy_O => lazy_O
  | lazy_S fn => lazy_plus m $ lazy_mult (fn tt) m
  end.
*)

(*
Fixpoint lazy_eq n m : lazy_nat -> lazy_nat -> Prop :=
  match n with
  | lazy_O => match m with lazy_O => tt
  |  
*)


(* lame: notation hiervoor in canonical names *)
Definition lazy_plus_1 n := lazy_S $ fun _ => n.
Definition lazy_1 := lazy_plus_1 lazy_O.
Definition lazy_2 := lazy_plus_1 lazy_1.
Definition lazy_3 := lazy_plus_1 lazy_2.
Definition lazy_4 := lazy_plus_1 lazy_3.

(* Eval compute in lazy_mult lazy_2 lazy_3. *)

(* Proof that lazy_nat is a Ring *)
Inductive lazy_nat_eq : Equiv lazy_nat :=
  | lazy_nat_eq_0 : lazy_O = lazy_O
  | lazy_nat_eq_S : ∀ x y u, x u = y u → lazy_S x = lazy_S y.
Existing Instance lazy_nat_eq.

(*
 Print Equiv.
 Equiv = λ A : Type, relation A
     : Type → Type

 Print relation.
 relation = λ A : Type, A → A → Prop
     : Type → Type
*)

Instance: Reflexive lazy_nat_eq.
Proof.
  intros x. induction x.
   now apply lazy_nat_eq_0.
  apply lazy_nat_eq_S with (u := tt).
  apply H.
Qed.

Instance: Transitive lazy_nat_eq.
Proof with (try repeat(try apply lazy_nat_eq_0; try apply lazy_nat_eq_S; auto)).
  intros x y z EQ_XY EQ_YZ.
  induction x.
   induction y.
    induction z. apply lazy_nat_eq_0.
    apply lazy_nat_eq_S with (u := tt).


Instance: Symmetric lazy_nat_eq.
Proof.
  intros x y H.
  induction x.
   induction y.
    apply lazy_nat_eq_0.
   apply lazy_nat_eq_0.
  intros.
   

Instance: Setoid lazy_nat.
Proof.
  split.

Admitted.    

   
(* Instance lazy_nat_eq : Equiv lazy_nat := eq. *)
Instance lazy_nat_0 : RingZero lazy_nat := lazy_O.
Instance lazy_nat_1 : RingOne lazy_nat := lazy_1.

Instance lazy_nat_plus : RingPlus lazy_nat :=
  fix lazy_plus n m :=
    match n with
    | lazy_O => m
    | lazy_S fn => lazy_S $ λ _, lazy_plus (fn ()) m
    end.

(* Notation from canonical_names *)
Instance lazy_nat_mult : RingMult lazy_nat :=
  fix lazy_mult n m :=
    match n with
    | lazy_O => lazy_O
    | lazy_S fn => m + lazy_mult (fn tt) m
    end.

Local Instance: LeftIdentity lazy_nat_plus lazy_nat_0.
Proof. easy. Qed.

Local Instance: RightIdentity lazy_nat_plus lazy_nat_0.
Proof.
  intros x. induction x.
   easy.
  simpl. (* rewrite (H ()). *)
Admitted.

Local Instance: Commutative lazy_nat_plus.
Proof.
  intros x y. induction x. 
  red.

Instance: SemiRing lazy_nat.
Proof.
  (* We unfold the [SemiRing] class, this gives us
     four more goals (check the definition of SemiRing).

     We unfold again, etc. immediatly trying to solve
     some goals using apply. *)
  repeat (split; try apply _).
Admitted.