lexicographic order proven well founded, checker extracted and verifying admission

5 files changed, 121 insertions, 1 deletions

diff --git a/theories/.lia.cache b/theories/.lia.cache
index 03484cb..239133a 100644
--- a/theories/.lia.cache
+++ b/theories/.lia.cache
diff --git a/theories/Decrease.vok b/theories/Decrease.vok
deleted file mode 100644
index e69de29..0000000
--- a/theories/Decrease.vok
+++ /dev/null
diff --git a/theories/Decrease.vos b/theories/Decrease.vos
deleted file mode 100644
index e69de29..0000000
--- a/theories/Decrease.vos
+++ /dev/null
diff --git a/theories/Lex.v b/theories/Lex.v
new file mode 100644
index 0000000..757a32c
--- /dev/null
+++ b/theories/Lex.v
@@ -0,0 +1,113 @@
+(* 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.
diff --git a/theories/dune b/theories/dune
index 3ef9648..57cccb6 100644
--- a/theories/dune
+++ b/theories/dune
@@ -15,6 +15,13 @@
   (setenv OCAMLPATH ""
    (run coqc -q DecreaseChecker.v))))
 
+(rule
+ (targets Lex.vo Lex.glob)
+ (deps Lex.v DecreaseChecker.vo)
+ (action
+  (setenv OCAMLPATH ""
+   (run coqc -q Lex.v))))
+
 (alias
  (name default)
- (deps Decrease.vo DecreaseChecker.vo))
+ (deps Decrease.vo DecreaseChecker.vo Lex.vo))