Theory Applicative_Test

(* Author: Joshua Schneider, ETH Zurich *)

section ‹Regression tests for applicative lifting›

theory Applicative_Test imports
  Stream_Algebra
  Applicative_Environment
  Applicative_List
  Applicative_Option
  Applicative_Set
  Applicative_Sum
  Abstract_AF
begin

unbundle applicative_syntax

subsection ‹Normal form conversion›

notepad
begin
  have "∀x. x = af_pure (λx. x) ⋄ x" by applicative_nf rule
  have "∀x. af_pure x = af_pure x" by applicative_nf rule
  have "∀f x. af_pure f ⋄ x = af_pure f ⋄ x" by applicative_nf rule
  have "∀f x y. af_pure f ⋄ x ⋄ y = af_pure f ⋄ x ⋄ y" by applicative_nf rule
  have "∀g f x. af_pure g ⋄ (f ⋄ x) = af_pure (λf x. g (f x)) ⋄ f ⋄ x" by applicative_nf rule
  have "∀f x y. f ⋄ x ⋄ y = af_pure (λf x y. f x y) ⋄ f ⋄ x ⋄ y" by applicative_nf rule
  have "∀g f x. g ⋄ (f ⋄ x) = af_pure (λg f x. g (f x)) ⋄ g ⋄ f ⋄ x" by applicative_nf rule
  have "∀f x. f ⋄ af_pure x = af_pure (λf. f x) ⋄ f" by applicative_nf rule
  have "∀x y. af_pure x ⋄ af_pure y = af_pure (x y)" by applicative_nf rule
  have "∀f x y. f ⋄ x ⋄ af_pure y = af_pure (λf x. f x y) ⋄ f ⋄ x" by applicative_nf rule
  have "∀f x y. af_pure f ⋄ x ⋄ af_pure y = af_pure (λx. f x y) ⋄ x" by applicative_nf rule
  have "∀f x y z. af_pure f ⋄ x ⋄ af_pure y ⋄ z = af_pure (λx z. f x y z) ⋄ x ⋄ z" by applicative_nf rule
  have "∀f x g y. af_pure f ⋄ x ⋄ (af_pure g ⋄ y) = af_pure (λx y. f x (g y)) ⋄ x ⋄ y" by applicative_nf rule
  have "∀f g x y. f ⋄ (g ⋄ x) ⋄ y = af_pure (λf g x y. f (g x) y) ⋄ f ⋄ g ⋄ x ⋄ y" by applicative_nf rule
  have "∀f g x y z. f ⋄ (g ⋄ x ⋄ y) ⋄ z = af_pure (λf g x y z. f (g x y) z) ⋄ f ⋄ g ⋄ x ⋄ y ⋄ z" by applicative_nf rule
  have "∀f g x y z. f ⋄ (g ⋄ (x ⋄ af_pure y)) ⋄ z = af_pure (λf g x z. f (g (x y)) z) ⋄ f ⋄ g ⋄ x ⋄ z" by applicative_nf rule
  have "∀f g x. f ⋄ (g ⋄ x ⋄ x) = af_pure (λf g x x'. f (g x x')) ⋄ f ⋄ g ⋄ x ⋄ x" by applicative_nf rule
  have "∀f x y. f x ⋄ y = af_pure (λf x. f x) ⋄ f x ⋄ y" by applicative_nf rule
next
  fix f :: "('a ⇒ 'b) af" and g :: "('b ⇒ 'c) af" and x
  have "g ⋄ (f ⋄ x) = af_pure (λg f x. g (f x)) ⋄ g ⋄ f ⋄ x" by applicative_nf rule
end
(* TODO automatic test for names of new variables *)

lemma "⋀f x::'a af. f ⋄ x = x"
apply applicative_nf
oops

subsection ‹Sets›

instantiation set :: (plus) plus
begin
  definition set_plus_def[applicative_unfold]: "(X::('a::plus)set) + Y = {plus} ⋄ X ⋄ Y"
  instance ..
end

lemma "(X :: _ :: semigroup_add set) + Y + Z = X + (Y + Z)"
by (fact add.assoc[applicative_lifted set])

instantiation set :: (semigroup_add) semigroup_add begin
instance proof
  fix X Y Z :: "'a set"
  from add.assoc
  show "X + Y + Z = X + (Y + Z)" by applicative_lifting
qed
end

instantiation set :: (ab_semigroup_add) ab_semigroup_add begin
instance proof
  fix X Y :: "'a set"
  from add.commute
  show "X + Y = Y + X" by applicative_lifting
qed
end

subsection ‹Sum type (a.k.a. either)›

lemma "Inl plus ⋄ (x :: nat + 'e list) ⋄ x = Inl (λx. 2 * x) ⋄ x"
by applicative_lifting simp

lemma "rel_sum (≤) (≤) (x :: nat + nat) (Inl Suc ⋄ x)"
proof -
  interpret either_af "(≤) :: nat ⇒ _" by unfold_locales (rule reflpI, simp)
  show ?thesis by applicative_lifting simp
qed


subsection ‹Streams›

lemma "(x::int stream) * sconst 0 = sconst 0"
by applicative_lifting simp

lemma "(x::int stream) * (y + z) = x * y + x * z"
by applicative_lifting algebra


definition "lift_streams xs = foldr (smap2 Cons) xs (sconst [])"

lemma lift_streams_Nil[applicative_unfold]: "lift_streams [] = sconst []"
unfolding lift_streams_def
by simp

lemma lift_streams_Cons[applicative_unfold]:
  "lift_streams (x # xs) = smap2 Cons x (lift_streams xs)"
unfolding lift_streams_def
by applicative_unfold

lemma stream_append_Cons: "smap2 append (smap2 Cons x ys) zs = smap2 Cons x (smap2 append ys zs)"
by applicative_lifting simp

lemma lift_streams_append[applicative_unfold]:
  "lift_streams (xs @ ys) = smap2 append (lift_streams xs) (lift_streams ys)"
proof (induction xs)
  case Nil
  (*
    case could be proved directly if "lift_streams ([] @ ys) = lift_streams ys" is solved
    in head_cong_tac (invoke simplifier?) -- but only with applicative_nf
  *)
  have "lift_streams ys = sconst append ⋄ lift_streams [] ⋄ lift_streams ys"
    by applicative_lifting simp
  thus ?case by applicative_unfold
next
  case (Cons x xs)
  with stream_append_Cons  (* the actual lifted fact *)
  show ?case by applicative_unfold (rule sym)
qed

lemma "lift_streams (rev x) = smap rev (lift_streams x)"
proof (induction x)
  case Nil
  have "lift_streams [] = smap rev (lift_streams [])"
    by applicative_lifting simp
  thus ?case by simp
next
  case (Cons x xs)
  have "∀y ys. rev ys @ [y] = rev (y # ys)" by simp
  hence "∀y ys. smap2 append (smap rev ys) (smap2 Cons y (sconst [])) = smap rev (smap2 Cons y ys)"
    by applicative_lifting simp
  with Cons.IH show ?case by applicative_unfold blast
qed

definition [applicative_unfold]: "sconcat xs = smap concat xs"

lemma "sconcat (lift_streams [sconst ''Hello '', sconst ''world!'']) = sconst ''Hello world!''"
by applicative_lifting simp


subsection ‹Relators›

lemma "rel_fun (=) (≤) (const (0::nat)) x"
by applicative_lifting simp

lemma "list_all2 (⊆) (map (λ_. {}) x) (map set x)"
by applicative_nf simp

lemma "x = Some a ⟹ rel_option (≤) (map_option (λ_. a) x) (map_option Suc x)"
by applicative_lifting simp

schematic_goal "∀g f x. rel_sum ?R (=) (ap_either f x) (ap_either (ap_either (Inl g) f) x)"
apply applicative_lifting
oops

schematic_goal "stream_all2 ?R (?f ⋄ (pure ?g ⋄ ?x + ?y)) (?x + ?z)"
apply applicative_lifting
oops


print_applicative

end