test.agda

module test where

open import Data.Nat
open import Data.Bool using (Bool; if_then_else_; true; false; _∧_)
open import Data.Product
import Relation.Binary.PropositionalEquality as Eq
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; _≡⟨_⟩_; _∎)
open Eq using (_≡_; refl; cong; sym)
open import Function.Equality using (_∘_)

data type : Set where
  tNat : type
  tBool : type
  tProd : type -> type -> type

data exp : type -> Set where
  NConst : ℕ -> exp tNat
  Plus : exp tNat -> exp tNat -> exp tNat
  Eq : exp tNat -> exp tNat -> exp tBool
  BConst : Bool -> exp tBool
  And : exp tBool -> exp tBool -> exp tBool
  Iff : ∀ {t} -> exp tBool -> exp t -> exp t -> exp t
  Pair : ∀ {t1 t2} -> exp t1 -> exp t2 -> exp (tProd t1 t2)
  Fst : ∀ {t1 t2} -> exp (tProd t1 t2) -> exp t1
  Snd : ∀ {t1 t2} -> exp (tProd t1 t2) -> exp t2

typeDenote : type -> Set
typeDenote tNat = ℕ
typeDenote tBool = Bool
typeDenote (tProd t1 t2) = typeDenote t1 × typeDenote t2

eqnat : ℕ → ℕ → Bool
eqnat zero zero = true
eqnat zero (suc n2) = false
eqnat (suc n1) zero = false
eqnat (suc n1) (suc n2) = eqnat n1 n2

expDenote : ∀ {t} -> exp t -> typeDenote t
expDenote  (NConst x) = x
expDenote  (Plus e e₁) = expDenote e + expDenote e₁
expDenote  (Eq e e₁) = eqnat (expDenote e) (expDenote e₁)
expDenote  (BConst x) = x
expDenote  (And e e₁) = expDenote e ∧ expDenote e₁
expDenote  (Iff  e e₁ e₂) = if (expDenote e) then expDenote e₁ else expDenote e₂
expDenote  (Pair e e₁) = expDenote e , expDenote e₁
expDenote  (Fst e) = proj₁ (expDenote e)
expDenote  (Snd e) = proj₂ (expDenote e)

smartplus : exp tNat -> exp tNat -> exp tNat
smartplus (NConst n1) (NConst n2)  = NConst (n1 + n2)
smartplus e1 e2 = Plus e1 e2

smartpluscorrect : ∀ e1 e2 -> expDenote e1 + expDenote e2 ≡ expDenote (smartplus e1 e2)
smartpluscorrect (NConst _) (NConst _) = refl
smartpluscorrect (NConst _) (Plus _ _) = refl
smartpluscorrect (NConst _) (Iff _ _ _) = refl
smartpluscorrect (NConst _) (Fst _) = refl
smartpluscorrect (NConst _) (Snd _) = refl
smartpluscorrect (Plus _ _) _ = refl
smartpluscorrect (Iff _ _ _) _ = refl
smartpluscorrect (Fst _) _ = refl
smartpluscorrect (Snd _) _ = refl

smarteq : exp tNat -> exp tNat -> exp tBool
smarteq (NConst n1) (NConst n2)  = BConst (eqnat n1 n2)
smarteq e1 e2 = Eq e1 e2

smarteqcorrect : ∀ e1 e2 -> expDenote (Eq e1 e2) ≡ expDenote (smarteq e1 e2)
smarteqcorrect (NConst _) (NConst _) = refl
smarteqcorrect (NConst _) (Plus _ _) = refl
smarteqcorrect (NConst _) (Iff _ _ _) = refl
smarteqcorrect (NConst _) (Fst _) = refl
smarteqcorrect (NConst _) (Snd _) = refl
smarteqcorrect (Plus _ _) _ = refl
smarteqcorrect (Iff _ _ _) _ = refl
smarteqcorrect (Fst _) _ = refl
smarteqcorrect (Snd _) _ = refl

smartand : exp tBool -> exp tBool -> exp tBool
smartand (BConst n1) (BConst n2)  = BConst (n1 ∧ n2)
smartand e1 e2 = And e1 e2

smartandcorrect : ∀ e1 e2 -> expDenote (And e1 e2) ≡ expDenote (smartand e1 e2)
smartandcorrect (BConst _) (BConst _) = refl
smartandcorrect (BConst _) (And _ _) = refl
smartandcorrect (BConst _) (Iff _ _ _) = refl
smartandcorrect (BConst _) (Fst _) = refl
smartandcorrect (BConst _) (Snd _) = refl
smartandcorrect (BConst _) (Eq _ _) = refl
smartandcorrect (And _ _) _ = refl
smartandcorrect (Iff _ _ _) _ = refl
smartandcorrect (Fst _) _ = refl
smartandcorrect (Snd _) _ = refl
smartandcorrect (Eq _ _) _ = refl

smartif : ∀ {t} -> exp tBool -> exp t -> exp t -> exp t
smartif (BConst true) t e  = t
smartif (BConst false) t e  = e
smartif i t e  = Iff i t e

smartifcorrect : ∀ {t} -> ∀ e1 (e2 e3 : exp t) -> expDenote (Iff e1 e2 e3) ≡ expDenote (smartif e1 e2 e3)
smartifcorrect (BConst true) _ _ = refl
smartifcorrect (BConst false) _ _ = refl
smartifcorrect (And _ _) _ _ = refl
smartifcorrect (Iff _ _ _) _ _ = refl
smartifcorrect (Fst _) _ _ = refl
smartifcorrect (Snd _) _ _ = refl
smartifcorrect (Eq _ _) _ _ = refl

smartfst : ∀ {t1 t2} -> exp (tProd t1 t2) -> exp t1
smartfst (Pair e1 e2)  = e1
smartfst e = Fst e

smartfstcorrect : ∀ {t1 t2} -> ∀ (e : exp (tProd t1 t2)) -> expDenote (Fst e) ≡ expDenote (smartfst e)
smartfstcorrect (Pair _ _)  = refl
smartfstcorrect (Iff _ _ _) = refl
smartfstcorrect (Fst _) = refl
smartfstcorrect (Snd _) = refl

smartsnd : ∀ {t1 t2} -> exp (tProd t1 t2) -> exp t2
smartsnd (Pair e1 e2)  = e2
smartsnd e = Snd e

smartsndcorrect : ∀ {t1 t2} -> ∀ (e : exp (tProd t1 t2)) -> expDenote (Snd e) ≡ expDenote (smartsnd e)
smartsndcorrect (Pair _ _)  = refl
smartsndcorrect (Iff _ _ _) = refl
smartsndcorrect (Fst _) = refl
smartsndcorrect (Snd  _) = refl

cfold : ∀ {t} -> exp t -> exp t
cfold (NConst x) = NConst x
cfold {t} (Plus e e₁) = smartplus (cfold e) (cfold e₁)
cfold (Eq e e₁) = smarteq (cfold e) (cfold e₁)
cfold (BConst x) = BConst x
cfold (And e e₁) =  smartand (cfold e) (cfold e₁)
cfold (Iff e e₁ e₂) = smartif (cfold e) (cfold e₁) (cfold e₂)
cfold (Pair e e₁) = Pair (cfold e) (cfold e₁)
cfold (Fst e) = smartfst (cfold e)
cfold (Snd e) = smartsnd (cfold e)


cfoldcorrect : ∀ {t} -> ∀ (e : exp t) -> expDenote e ≡ expDenote (cfold e)
cfoldcorrect (NConst x)  = refl
cfoldcorrect (Plus e e₁)  = begin
  expDenote e + expDenote e₁
  ≡⟨ cong (λ x -> x + expDenote e₁)  (cfoldcorrect e) ⟩
  expDenote (cfold e) + expDenote e₁
  ≡⟨ cong (λ x -> expDenote (cfold e) + x)  (cfoldcorrect e₁) ⟩
  expDenote (cfold e) + expDenote (cfold e₁)
  ≡⟨ smartpluscorrect (cfold e) (cfold e₁) ⟩
  expDenote (smartplus (cfold e) (cfold e₁))
  ∎
cfoldcorrect (Eq e e₁)  = begin
  eqnat (expDenote e) (expDenote e₁)
  ≡⟨ cong (λ x -> eqnat x (expDenote e₁))  (cfoldcorrect e) ⟩
  eqnat (expDenote (cfold e)) (expDenote e₁)
  ≡⟨ cong (λ x -> eqnat (expDenote (cfold e)) x)  (cfoldcorrect e₁) ⟩
  eqnat (expDenote (cfold e)) (expDenote (cfold e₁))
  ≡⟨ smarteqcorrect (cfold e) (cfold e₁) ⟩
  expDenote (smarteq (cfold e) (cfold e₁))
  ∎
cfoldcorrect (BConst x)  = refl
cfoldcorrect (And e e₁)  = begin
  expDenote e ∧ expDenote e₁
  ≡⟨ cong (λ x -> x ∧ expDenote e₁)  (cfoldcorrect e) ⟩
  expDenote (cfold e) ∧ expDenote e₁
  ≡⟨ cong (λ x -> expDenote (cfold e) ∧ x)  (cfoldcorrect e₁) ⟩
  expDenote (cfold e) ∧ expDenote (cfold e₁)
  ≡⟨ smartandcorrect (cfold e) (cfold e₁) ⟩
  expDenote (smartand (cfold e) (cfold e₁))
  ∎
cfoldcorrect (Iff e e₁ e₂)  = begin
  (if (expDenote e) then (expDenote e₁) else (expDenote e₂))
  ≡⟨ cong (λ x ->  if x then (expDenote e₁) else (expDenote e₂))  (cfoldcorrect e) ⟩
  (if (expDenote (cfold e)) then (expDenote e₁) else (expDenote e₂))
  ≡⟨ cong (λ x ->  if (expDenote (cfold e)) then x else (expDenote e₂))  (cfoldcorrect e₁) ⟩
  (if (expDenote (cfold e)) then (expDenote (cfold e₁)) else (expDenote e₂))
  ≡⟨ cong (λ x ->  if (expDenote (cfold e)) then (expDenote (cfold e₁)) else x)  (cfoldcorrect e₂) ⟩
  (if (expDenote (cfold e)) then (expDenote (cfold e₁)) else (expDenote (cfold e₂)))
  ≡⟨ smartifcorrect (cfold e) (cfold e₁) (cfold e₂) ⟩
  expDenote (smartif (cfold e) (cfold e₁) (cfold e₂))
  ∎
cfoldcorrect (Pair e e₁)  = begin
  expDenote e , expDenote e₁
  ≡⟨ cong (λ x -> x , expDenote e₁)  (cfoldcorrect e) ⟩
  expDenote (cfold e) , expDenote e₁
  ≡⟨ cong (λ x -> expDenote (cfold e) , x)  (cfoldcorrect e₁) ⟩
  expDenote (cfold e) , expDenote (cfold e₁)
  ∎
cfoldcorrect (Fst e)  = begin
  proj₁ (expDenote e)
  ≡⟨ cong proj₁  (cfoldcorrect e) ⟩
  proj₁ (expDenote (cfold e))
  ≡⟨ smartfstcorrect (cfold e)  ⟩
  expDenote (smartfst (cfold e))
  ∎
cfoldcorrect (Snd e)  =  begin
  proj₂ (expDenote e)
  ≡⟨ cong proj₂  (cfoldcorrect e) ⟩
  proj₂ (expDenote (cfold e))
  ≡⟨ smartsndcorrect (cfold e)  ⟩
  expDenote (smartsnd (cfold e))
  ∎

test.v

(* same example in Coq using the Equations plugin.
   Proof size is now constant instead of quadratic.,
   but program is as straightforward as in Agda. *)

Require Import Arith Omega.
From Equations Require Import Equations.
Require Import Coq.Bool.Bool.

Set Implicit Arguments.
Set Asymmetric Patterns.


Inductive type : Set :=
| Nat : type
| Bool : type
| Prod : type -> type -> type.

Inductive exp : type -> Set :=
| NConst : nat -> exp Nat
| Plus : exp Nat -> exp Nat -> exp Nat
| Eq : exp Nat -> exp Nat -> exp Bool

| BConst : bool -> exp Bool
| And : exp Bool -> exp Bool -> exp Bool
| If : forall t, exp Bool -> exp t -> exp t -> exp t

| Pair : forall t1 t2, exp t1 -> exp t2 -> exp (Prod t1 t2)
| Fst : forall t1 t2, exp (Prod t1 t2) -> exp t1
| Snd : forall t1 t2, exp (Prod t1 t2) -> exp t2.

Fixpoint typeDenote (t : type) : Set :=
  match t with
    | Nat => nat
    | Bool => bool
    | Prod t1 t2 => typeDenote t1 * typeDenote t2
  end%type.

Fixpoint expDenote t (e : exp t) : typeDenote t :=
  match e with
    | NConst n => n
    | Plus e1 e2 => expDenote e1 + expDenote e2
    | Eq e1 e2 => if eq_nat_dec (expDenote e1) (expDenote e2) then true else false

    | BConst b => b
    | And e1 e2 => expDenote e1 && expDenote e2
    | If _ e' e1 e2 => if expDenote e' then expDenote e1 else expDenote e2

    | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
    | Fst _ _ e' => fst (expDenote e')
    | Snd _ _ e' => snd (expDenote e')
  end.

Derive NoConfusion EqDec for type.
Derive Signature NoConfusion  for exp. 

Equations smartplus(e1 : exp Nat)(e2: exp Nat) : exp Nat :=
  smartplus (NConst n1) (NConst n2) := NConst (n1 + n2) ;
  smartplus e1 e2 := Plus e1 e2.

Equations smarteq(e1 : exp Nat)(e2: exp Nat) : exp Bool :=
  smarteq (NConst n1) (NConst n2) := BConst (if (eq_nat_dec n1 n2) then true else false) ;
  smarteq e1 e2 := Eq e1 e2.

Equations smartand(e1 : exp Bool)(e2: exp Bool) : exp Bool :=
  smartand (BConst n1) (BConst n2) := BConst (n1 && n2) ;
  smartand e1 e2 := And e1 e2.

Equations smartif {t} (e1 : exp Bool)(e2: exp t)(e3: exp t) : exp t :=
  smartif (BConst n1) e2 e3 := if n1 then e2 else e3 ;
  smartif e1 e2 e3 := If e1 e2 e3.

Equations smartfst {t1 t2} (e: exp (Prod t1 t2)) : exp t1 :=
  smartfst (Pair e1 e2) := e1;
  smartfst e := Fst e.

Equations smartsnd {t1 t2} (e: exp (Prod t1 t2)) : exp t2 :=
  smartsnd (Pair e1 e2) := e2;
  smartsnd e := Snd e.

Equations cfold {t} (e: exp t) : exp t :=
  cfold (NConst n) := NConst n ;
  cfold (Plus e1 e2) := smartplus (cfold e1) (cfold e2); 
  cfold (Eq e1 e2) := smarteq (cfold e1) (cfold e2); 
  cfold (BConst x) := BConst x; 
  cfold (And e1 e2) := smartand (cfold e1) (cfold e2); 
  cfold (If e1 e2 e3) := smartif (cfold e1) (cfold e2) (cfold e3); 
  cfold (Pair e1 e2) := Pair (cfold e1) (cfold e2);
  cfold (Fst e) := smartfst (cfold e); 
  cfold (Snd e) := smartsnd (cfold e).

Lemma cfoldcorrect: forall t (e: exp t), expDenote e = expDenote (cfold e).
intros; funelim (cfold e); simpl; try reflexivity;
 repeat match goal with [ H : expDenote ?e = _ |- context[expDenote ?e]] => rewrite H end;
try (match goal with [ |- _ = expDenote ?f] => funelim f end); simpl;
 repeat match goal with [ H : _ = cfold ?e |- _] => rewrite <- H end; try reflexivity;
 repeat match goal with [  |- context[if ?e then _ else _]] => destruct e end; try reflexivity.
Qed.