prove denote rules for Hedge.Elem

Author: awalterschulze

Validator/Hedge/Elem.lean

@@ -3,7 +3,7 @@ import Validator.Std.List
 import Validator.Regex.Regex
 import Validator.Hedge.Grammar
 
-namespace Hedge.Elem
+namespace Hedge.Grammar.Elem
 
 theorem decreasing_or_l {α: Type} {σ: Type} [SizeOf σ] (r1 r2: Regex σ) (xs: Hedge α):
   Prod.Lex
@@ -148,11 +148,9 @@ def lift_symbol {x: Hedge.Node α}
     simp_all only [List.mem_flatMap, List.mem_cons, or_true]
   )
 
--- denote_elem is an alternative version of Regex.denote that is later proven to be equivalent definitions.
--- The difference is that the denote_symbol function now has a relationship with the original input list, List.InfixOf.
--- This relationship is used for proving termination of regular expressions on trees.
+-- Hedge.Elem.Rule.denote_elem is an alternative version of Hedge.Grammar.Rule.denote.
 -- The only other changes is that denote_elem contains unfolded versions of Language.or, Language.concat_n and Language.star_n.
-def denote_elem
+def Rule.denote_elem
   {α: Type} {φ: Type}
   (G: Hedge.Grammar n φ)
   (r: Hedge.Grammar.Rule n φ) (xs: Hedge α)
@@ -189,3 +187,117 @@ def denote_elem
     · apply denote_elem_sizeOf_concat_right
     · apply denote_elem_sizeOf_star_left
     · apply denote_elem_sizeOf_star_right
+
+def Rule.denote {α: Type} {φ: Type}
+  (G: Hedge.Grammar n φ) (Φ: φ -> α -> Prop)
+  (r: Hedge.Grammar.Rule n φ) (xs: Hedge α): Prop :=
+  Rule.denote_elem G r xs (fun p x' => Φ p x'.val)
+
+theorem denote_emptyset {α: Type} {φ: Type} (G: Hedge.Grammar n φ) (Φ: φ -> α -> Prop):
+  Rule.denote G Φ Regex.emptyset = Regex.Language.emptyset := by
+  unfold Rule.denote
+  simp only [Rule.denote_elem]
+
+theorem denote_emptystr {α: Type} {φ: Type} (G: Hedge.Grammar n φ) (Φ: φ -> α -> Prop):
+  Rule.denote G Φ Regex.emptystr = Regex.Language.emptystr := by
+  unfold Rule.denote
+  simp only [Rule.denote_elem]
+
+theorem denote_symbol {α: Type} {φ: Type} (G: Hedge.Grammar n φ) (Φ: φ -> α -> Prop) [DecidableRel Φ] (s: Symbol n φ):
+  Rule.denote G Φ (Regex.symbol s) = Hedge.Language.tree (fun a => Φ s.1 a) (Rule.denote G Φ (G.lookup s.2)) := by
+  unfold Rule.denote
+  unfold Hedge.Language.tree
+  funext xs
+  simp only
+  cases xs with
+  | nil =>
+    rw [Rule.denote_elem]
+    simp only [List.ne_cons_self, decide_eq_true_eq, false_and, exists_const, exists_false]
+    intro x Φ h
+    contradiction
+  | cons x xs =>
+    cases xs with
+    | nil =>
+      rw [Rule.denote_elem]
+      simp only [List.cons.injEq, and_true, decide_eq_true_eq]
+      cases x with
+      | mk label children =>
+      simp only [Node.mk.injEq, ↓existsAndEq, and_true, exists_eq_left']
+      simp only [LabelIn.self, Node.getLabel]
+      simp_all only [eq_iff_iff, and_congr_right_iff]
+      intro a
+      obtain ⟨fst, snd⟩ := s
+      simp_all only
+      rfl
+    | cons x' xs =>
+      rw [Rule.denote_elem]
+      simp
+      intro x Φ h
+      simp at h
+
+theorem denote_or {α: Type} {φ: Type} (G: Hedge.Grammar n φ) (Φ: φ -> α -> Prop) (r1 r2: Rule n φ):
+  Rule.denote G Φ (Regex.or r1 r2) = Regex.Language.or (Rule.denote G Φ r1) (Rule.denote G Φ r2) := by
+  unfold Rule.denote
+  funext
+  simp only [Rule.denote_elem, Regex.Language.or]
+
+theorem denote_concat_n {α: Type} {φ: Type} (G: Hedge.Grammar n φ) (Φ: φ -> α -> Prop) (p q: Rule n φ):
+  Rule.denote G Φ (Regex.concat p q) = Regex.Language.concat_n (Rule.denote G Φ p) (Rule.denote G Φ q) := by
+  unfold Rule.denote
+  funext
+  simp only [Rule.denote_elem]
+  unfold Regex.Language.concat_n
+  rfl
+
+theorem unfold_denote_elem_star_n {α: Type} {φ: Type} (G: Hedge.Grammar n φ) (Φ: φ -> α -> Prop) (r: Rule n φ) (xs: Hedge α):
+  Rule.denote_elem G (Regex.star r) xs (fun p x' => Φ p x'.val)
+  = (match xs with
+    | [] => True
+    | (x'::xs') =>
+       ∃ (n: Fin xs.length),
+         (Rule.denote_elem G r (List.take (n + 1) (x'::xs')) (denote_symbol_lift_take (n + 1) (fun p x' => Φ p x'.val)))
+      /\ (Rule.denote_elem G (Regex.star r) (List.drop (n + 1) (x'::xs')) (denote_symbol_lift_drop (n + 1) (fun p x' => Φ p x'.val)))) := by
+  cases xs with
+  | nil =>
+    simp [Rule.denote_elem]
+  | cons x xs =>
+    cases xs with
+    | cons _ _ =>
+      simp only [Rule.denote_elem]
+    | nil =>
+      simp only [Rule.denote_elem]
+
+theorem denote_elem_star_n_iff {α: Type} {φ: Type} (G: Hedge.Grammar n φ) (Φ: φ -> α -> Prop) (r: Rule n φ) (xs: Hedge α):
+  Rule.denote_elem G (Regex.star r) xs (fun p x' => Φ p x'.val) <-> Regex.Language.star_n (fun xs' => Rule.denote_elem G r xs' (fun p x' => Φ p x'.val)) xs := by
+  rw [<- eq_iff_iff]
+  unfold Regex.Language.star_n
+  rw [unfold_denote_elem_star_n]
+  cases xs with
+  | nil =>
+    rfl
+  | cons x xs =>
+    simp only
+    congr
+    ext n
+    rw [<- eq_iff_iff]
+    unfold denote_symbol_lift_take
+    unfold denote_symbol_lift_drop
+    congr
+    simp only
+    simp only [LabelIn.mk]
+    simp only [List.length_cons, List.drop_succ_cons, eq_iff_iff]
+    rw [<- denote_elem_star_n_iff]
+  termination_by xs.length
+  decreasing_by
+    obtain ⟨n, hn⟩ := n
+    apply List.list_length_drop_lt_cons
+
+theorem denote_star_n_iff {α: Type} {φ: Type} (G: Hedge.Grammar n φ) (Φ: φ -> α -> Prop) (r: Rule n φ) (xs: Hedge α):
+  Rule.denote G Φ (Regex.star r) xs <-> Regex.Language.star_n (Rule.denote G Φ r) xs := by
+  unfold Rule.denote
+  rw [denote_elem_star_n_iff]
+
+theorem denote_star_n {α: Type} {φ: Type} (G: Hedge.Grammar n φ) (Φ: φ -> α -> Prop) (r: Rule n φ):
+  Rule.denote G Φ (Regex.star r) = Regex.Language.star_n (Rule.denote G Φ r) := by
+  funext
+  rw [denote_star_n_iff]

Validator/Hedge/Grammar.lean

@@ -239,7 +239,7 @@ theorem Rule.denote_concat {n: Nat} {α: Type}
   funext xs
   rw [Regex.Language.concat_n_is_concat]
 
-theorem denote_rule_star_n_iff {n: Nat} {α: Type}
+theorem denote_star_n_iff {n: Nat} {α: Type}
   {G: Grammar n φ} {Φ: φ -> α -> Bool} {r: Rule n φ} (xs: Hedge α):
   Rule.denote G Φ (Regex.star r) xs
   <->
@@ -263,7 +263,7 @@ theorem denote_rule_star_n_iff {n: Nat} {α: Type}
     simp only
     simp only [List.ElemOf.mk]
     simp
-    rw [<- denote_rule_star_n_iff]
+    rw [<- denote_star_n_iff]
     rw [Rule.denote]
   termination_by xs.length
   decreasing_by
@@ -276,15 +276,15 @@ theorem Rule.denote_star_n {n: Nat} {α: Type}
   =
   Regex.Language.star_n (Rule.denote G Φ r) := by
   funext xs
-  rw [denote_rule_star_n_iff]
+  rw [denote_star_n_iff]
 
 theorem Rule.denote_star {n: Nat} {α: Type}
   {G: Grammar n φ} {Φ: φ -> α -> Bool} {r: Rule n φ}:
   Rule.denote G Φ (Regex.star r)
   =
   Regex.Language.star_append (Rule.denote G Φ r) := by
   funext xs
-  rw [denote_rule_star_n_iff]
+  rw [denote_star_n_iff]
   rw [Regex.Language.star_append_is_star_n]
 
 def Rule.denote_onlyif {α: Type}