(* The executable admission checker, proven and extracted.

   Decrease.v states the abstract argument: strict containment
   decreases a well founded measure. This file carries the argument
   over to an executable checker faithful to lib/pattern.ml: terms
   keep their labels and leaf identities, the checker is a boolean
   function, and its soundness is proven, so extraction can replace
   the hand written OCaml. The equality functions supplied by the
   host and the conversion from Pattern.t are the remaining trusted
   seam. *)

From Stdlib Require Import Arith Lia Bool Wf_nat.

Section Checker.
  Variables (L A : Type).
  Variables (eqL : L -> L -> bool) (eqA : A -> A -> bool).

  (* Terms as the checker sees them: leaves carry their identity
     (variable name, scalar value), nodes carry labeled fields in
     canonical order. Mirrors Pattern.t through an injective
     conversion. *)
  Inductive term : Type :=
  | Leaf : A -> term
  | Node : fields -> term
  with fields : Type :=
  | FNil : fields
  | FCons : L -> term -> fields -> fields.

  Scheme term_mut := Induction for term Sort Prop
    with fields_mut := Induction for fields Sort Prop.
  Combined Scheme term_fields_mut from term_mut, fields_mut.

  Fixpoint term_eqb (x y : term) : bool :=
    match x, y with
    | Leaf a, Leaf b => eqA a b
    | Node f, Node g => fields_eqb f g
    | _, _ => false
    end
  with fields_eqb (f g : fields) : bool :=
    match f, g with
    | FNil, FNil => true
    | FCons l t r, FCons l' t' r' =>
        eqL l l' && term_eqb t t' && fields_eqb r r'
    | _, _ => false
    end.

  (* Strict containment: [sub] occurs somewhere inside the fields of
     [t], at depth one or more. *)
  Fixpoint contains (sub t : term) : bool :=
    match t with
    | Leaf _ => false
    | Node f => fields_contain sub f
    end
  with fields_contain (sub : term) (f : fields) : bool :=
    match f with
    | FNil => false
    | FCons _ t r => term_eqb t sub || contains sub t || fields_contain sub r
    end.

  Fixpoint size (t : term) : nat :=
    match t with
    | Leaf _ => 1
    | Node f => S (fields_size f)
    end
  with fields_size (f : fields) : nat :=
    match f with
    | FNil => 0
    | FCons _ t r => size t + fields_size r
    end.

  Hypothesis eqL_sound : forall x y, eqL x y = true -> x = y.
  Hypothesis eqA_sound : forall x y, eqA x y = true -> x = y.

  Lemma eqb_sound_all :
    (forall x, forall y, term_eqb x y = true -> x = y)
    /\ (forall f, forall g, fields_eqb f g = true -> f = g).
  Proof.
    apply term_fields_mut.
    - intros a y H; destruct y; simpl in H; [ f_equal; auto | discriminate ].
    - intros f IH y H; destruct y; simpl in H; [ discriminate | f_equal; auto ].
    - intros g H; destruct g; [ reflexivity | discriminate ].
    - intros l t IHt r IHr g H; destruct g; simpl in H; [ discriminate | ].
      rewrite !andb_true_iff in H; destruct H as [[Hl Ht] Hr].
      f_equal; auto.
  Qed.

  Definition term_eqb_sound := proj1 eqb_sound_all.

  Lemma contains_size_all :
    (forall t, forall sub, contains sub t = true -> size sub < size t)
    /\ (forall f, forall sub, fields_contain sub f = true -> size sub <= fields_size f).
  Proof.
    apply term_fields_mut.
    - intros a sub H; simpl in H; discriminate.
    - intros f IH sub H; simpl in H; simpl.
      specialize (IH _ H); lia.
    - intros sub H; simpl in H; discriminate.
    - intros l t IHt r IHr sub H; simpl in H; simpl.
      rewrite !orb_true_iff in H; destruct H as [[He | Hc] | Hr].
      + apply term_eqb_sound in He; subst; lia.
      + specialize (IHt _ Hc); lia.
      + specialize (IHr _ Hr); lia.
  Qed.

  Definition contains_decreases := proj1 contains_size_all.

  (* The checker's acceptance order is well founded: any chain of
     recursive unfoldings whose argument the checker accepts is
     finite. This is what admission buys at runtime. *)
  Definition decrease (b a : term) : Prop := contains b a = true.

  Theorem decrease_well_founded : well_founded decrease.
  Proof.
    apply well_founded_lt_compat with (f := size).
    intros x y H; apply contains_decreases; exact H.
  Qed.

End Checker.