blob: 757a32cf25dbfdebe2ea71a5729acd43a222ddff (
plain) (
tree)
|
|
(* 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.
|
