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