(* The lexicographic extension of the containment order, proven well
   founded, with an executable checker for extraction.

   Admission finds a measure (an ordered list of labels) by
   heuristic search; that search stays untrusted. What must be
   trusted is only this: that a call whose projected arguments pass
   [lex_ltb] really is smaller in a well founded order. Soundness of
   the checker and well foundedness of the order are proven here;
   the OCaml side verifies every intra-component call with the
   extracted checker. *)

From Stdlib Require Import List Arith Lia Bool Wf_nat.
Import ListNotations.
Require Import DecreaseChecker.

Section LexOrder.
  Variables (L A : Type).
  Variables (eqL : L -> L -> bool) (eqA : A -> A -> bool).
  Hypothesis eqL_sound : forall x y, eqL x y = true -> x = y.
  Hypothesis eqA_sound : forall x y, eqA x y = true -> x = y.

  Notation term := (term L A).
  Notation containsb := (contains L A eqL eqA).
  Notation eqb := (term_eqb L A eqL eqA).
  Notation eqb_sound := (term_eqb_sound L A eqL eqA eqL_sound eqA_sound).
  Notation dec_sizes :=
    (contains_decreases L A eqL eqA eqL_sound eqA_sound).

  (* b strictly below a in the containment order. *)
  Definition below (b a : term) : Prop := containsb b a = true.

  (* Lexicographic order on argument tuples: strict decrease at the
     head, or an equal head and decrease in the tail. Lengths agree,
     which projection through a fixed measure guarantees. *)
  Inductive lex_lt : list term -> list term -> Prop :=
  | lex_hd : forall b a bs aas,
      below b a -> length bs = length aas -> lex_lt (b :: bs) (a :: aas)
  | lex_tl : forall a bs aas,
      lex_lt bs aas -> lex_lt (a :: bs) (a :: aas).

  Fixpoint lex_ltb (bs aas : list term) : bool :=
    match bs, aas with
    | b :: bs', a :: aas' =>
        (containsb b a && Nat.eqb (length bs') (length aas'))
        || (eqb b a && lex_ltb bs' aas')
    | _, _ => false
    end.

  Lemma lex_ltb_sound : forall bs aas, lex_ltb bs aas = true -> lex_lt bs aas.
  Proof.
    induction bs as [| b bs IH]; intros [| a aas] H; simpl in H;
      try discriminate.
    rewrite orb_true_iff, !andb_true_iff in H.
    destruct H as [[Hc Hl] | [He Hr]].
    - apply lex_hd; [ exact Hc | apply Nat.eqb_eq; exact Hl ].
    - apply eqb_sound in He; subst a. apply lex_tl; auto.
  Qed.

  Lemma lex_lt_length : forall bs aas, lex_lt bs aas -> length bs = length aas.
  Proof.
    intros bs aas H; induction H; simpl; auto.
  Qed.

  Lemma lex_lt_inv : forall y a bs,
    lex_lt y (a :: bs) ->
    (exists b ys, y = b :: ys /\ below b a /\ length ys = length bs)
    \/ (exists ys, y = a :: ys /\ lex_lt ys bs).
  Proof.
    intros y a bs H; inversion H; subst; [ left | right ]; eauto 7.
  Qed.

  (* Well foundedness, by induction on tuple length. The head is
     handled by Acc in the containment order (well founded via the
     size measure of DecreaseChecker); the tail by the induction
     hypothesis on the shorter length. *)
  Lemma below_acc : forall a, Acc below a.
  Proof.
    apply well_founded_lt_compat with (f := size L A).
    intros x y H. apply dec_sizes. exact H.
  Qed.

  Lemma lex_wf_len :
    forall n bs, length bs = n -> Acc lex_lt bs.
  Proof.
    induction n as [| m IHm]; intros bs Hlen.
    - destruct bs; [ | simpl in Hlen; discriminate ].
      constructor; intros y Hy; inversion Hy.
    - destruct bs as [| a bs]; simpl in Hlen; [ discriminate | ].
      injection Hlen as Hlen.
      revert bs Hlen.
      assert (Hacc_a : Acc below a) by apply below_acc.
      induction Hacc_a as [a _ IHa].
      intros bs Hlen.
      assert (Hacc_bs : Acc lex_lt bs) by (apply IHm; exact Hlen).
      revert Hlen.
      induction Hacc_bs as [bs Hbs IHbs].
      intros Hlen.
      constructor; intros y Hy.
      destruct (lex_lt_inv _ _ _ Hy)
        as [ (b & ys & -> & Hb & Hl) | (ys & -> & Hlt) ].
      + (* head decreased; the tail is any list of length m *)
        apply IHa; [ exact Hb | congruence ].
      + (* equal head; the tail decreased *)
        apply IHbs; [ exact Hlt | ].
        rewrite (lex_lt_length _ _ Hlt); exact Hlen.
  Qed.

  Theorem lex_well_founded : well_founded lex_lt.
  Proof.
    intros bs. apply lex_wf_len with (n := length bs). reflexivity.
  Qed.

End LexOrder.