Library hydras.rpo.rpo
by Evelyne Contejean, LRI
From Coq Require Import List Relations Wellfounded Arith Wf_nat Lia.
From hydras Require Import more_list list_permut dickson term.
A non-dependent version of lexicographic extension.
Definition lex (A B : Set)
(eq_A_dec : ∀ a1 a2, {a1=a2}+{a1≠a2})
(o1 : relation A) (o2 : relation B) (s t : _ × _) :=
match s, t with (s1,s2), (t1,t2) ⇒
if eq_A_dec s1 t1 then o2 s2 t2 else o1 s1 t1
end.
Transitivity of lexicographic extension.
Lemma lex_trans :
∀ (A B : Set) eq_A_dec o1 o2,
antisymmetric A o1 → transitive A o1 → transitive B o2 →
transitive _ (lex _ _ eq_A_dec o1 o2).
Well-foundedness of lexicographic extension.
Lemma wf_lex :
∀ A B eq_A_dec o1 o2, well_founded o1 → well_founded o2 →
well_founded (lex A B eq_A_dec o1 o2).
Module Type Precedence.
Parameter A : Set.
Parameter prec : relation A.
Inductive status_type : Set :=
| Lex : status_type
| Mul : status_type.
Parameter status : A → status_type.
Axiom prec_dec : ∀ a1 a2 : A, {prec a1 a2} + {¬ prec a1 a2}.
Axiom prec_antisym : ∀ s, prec s s → False.
Axiom prec_transitive : transitive A prec.
End Precedence.
Module Type RPO.
Declare Module T : term.Term.
Declare Module P : Precedence with Definition A:= T.symbol.
Import T.
Import P.
Declare Module LP : list_permut.Permut with Definition DS.A:=term.
Import LP.
Inductive rpo : term → term → Prop :=
| Subterm : ∀ f l t s, In s l → rpo_eq t s → rpo t (Term f l)
| Top_gt :
∀ f g l l', prec g f →
(∀ s', In s' l' → rpo s' (Term f l)) →
rpo (Term g l') (Term f l)
| Top_eq_lex :
∀ f l l', status f = Lex → rpo_lex l' l →
(∀ s', In s' l' → rpo s' (Term f l)) →
rpo (Term f l') (Term f l)
| Top_eq_mul :
∀ f l l', status f = Mul → rpo_mul l' l →
rpo (Term f l') (Term f l)
with rpo_eq : term → term → Prop :=
| Eq : ∀ t, rpo_eq t t
| Lt : ∀ s t, rpo s t → rpo_eq s t
with rpo_lex : list term → list term → Prop :=
| List_gt :
∀ s t l l', rpo s t → length l = length l' →
rpo_lex (s :: l) (t :: l')
| List_eq : ∀ s l l', rpo_lex l l' →
rpo_lex (s :: l) (s :: l')
with rpo_mul : list term → list term → Prop :=
| List_mul :
∀ a lg ls lc l l',
list_permut l' (ls ++ lc) →
list_permut l (a :: lg ++ lc) →
(∀ b, In b ls → ∃ a', In a' (a :: lg) ∧ rpo b a') →
rpo_mul l' l.
| Subterm : ∀ f l t s, In s l → rpo_eq t s → rpo t (Term f l)
| Top_gt :
∀ f g l l', prec g f →
(∀ s', In s' l' → rpo s' (Term f l)) →
rpo (Term g l') (Term f l)
| Top_eq_lex :
∀ f l l', status f = Lex → rpo_lex l' l →
(∀ s', In s' l' → rpo s' (Term f l)) →
rpo (Term f l') (Term f l)
| Top_eq_mul :
∀ f l l', status f = Mul → rpo_mul l' l →
rpo (Term f l') (Term f l)
with rpo_eq : term → term → Prop :=
| Eq : ∀ t, rpo_eq t t
| Lt : ∀ s t, rpo s t → rpo_eq s t
with rpo_lex : list term → list term → Prop :=
| List_gt :
∀ s t l l', rpo s t → length l = length l' →
rpo_lex (s :: l) (t :: l')
| List_eq : ∀ s l l', rpo_lex l l' →
rpo_lex (s :: l) (s :: l')
with rpo_mul : list term → list term → Prop :=
| List_mul :
∀ a lg ls lc l l',
list_permut l' (ls ++ lc) →
list_permut l (a :: lg ++ lc) →
(∀ b, In b ls → ∃ a', In a' (a :: lg) ∧ rpo b a') →
rpo_mul l' l.
Axiom rpo_closure :
∀ s t u,
(rpo t s → rpo u t → rpo u s) ∧
(rpo s t → rpo t s → False) ∧
(rpo s s → False) ∧
(rpo_eq s t → rpo_eq t s → s = t).
Axiom rpo_trans : ∀ s t u, rpo t s → rpo u t → rpo u s.
Axiom rpo_add_context :
∀ p ctx s t, rpo s t → is_a_pos ctx p = true →
rpo (replace_at_pos ctx s p) (replace_at_pos ctx t p).
End RPO.
Module Make (T1: term.Term)
(P1 : Precedence with Definition A := T1.symbol)
<: RPO.
Module T := T1.
Module P := P1.
Import T.
Import P.
Module LP := list_permut.Make (Term_eq_dec).
Import LP.
Definition o_size s t := size s < size t.
Lemma wf_size : well_founded o_size.
Definition size2 s := match s with (s1,s2) ⇒ (size s1, size s2) end.
Definition o_size2 s t := lex _ _ eq_nat_dec lt lt (size2 s) (size2 t).
Lemma wf_size2 : well_founded o_size2.
Definition size3 s := match s with (s1,s2) ⇒ (size s1, size2 s2) end.
Definition o_size3 s t :=
lex _ _ eq_nat_dec lt (lex _ _ eq_nat_dec lt lt) (size3 s) (size3 t).
Lemma wf_size3 : well_founded o_size3.
Lemma lex1 :
∀ s f l t1 u1 t2 u2, In s l → o_size3 (s,(t1,u1)) (Term f l,(t2,u2)).
Lemma lex1_bis :
∀ a f l t1 u1 t2 u2, o_size3 (Term f l,(t1,u1)) (Term f (a::l),(t2,u2)).
Lemma lex2 :
∀ t f l s u1 u2, In t l → o_size3 (s,(t,u1)) (s,(Term f l, u2)).
Lemma lex3 :
∀ u f l s t, In u l → o_size3 (s,(t,u)) (s,(t,Term f l)).
Lemma o_size3_trans : transitive _ o_size3.
Inductive rpo : term → term → Prop :=
| Subterm : ∀ f l t s, In s l → rpo_eq t s → rpo t (Term f l)
| Top_gt :
∀ f g l l', prec g f →
(∀ s', In s' l' → rpo s' (Term f l)) →
rpo (Term g l') (Term f l)
| Top_eq_lex :
∀ f l l', status f = Lex → rpo_lex l' l →
(∀ s', In s' l' → rpo s' (Term f l)) →
rpo (Term f l') (Term f l)
| Top_eq_mul :
∀ f l l', status f = Mul → rpo_mul l' l →
rpo (Term f l') (Term f l)
with rpo_eq : term → term → Prop :=
| Eq : ∀ t, rpo_eq t t
| Lt : ∀ s t, rpo s t → rpo_eq s t
with rpo_lex : list term → list term → Prop :=
| List_gt :
∀ s t l l', rpo s t → length l = length l' →
rpo_lex (s :: l) (t :: l')
| List_eq : ∀ s l l', rpo_lex l l' → rpo_lex (s :: l) (s :: l')
with rpo_mul : list term → list term → Prop :=
| List_mul :
∀ a lg ls lc l l',
list_permut l' (ls ++ lc) →
list_permut l (a :: lg ++ lc) →
(∀ b, In b ls → ∃ a', In a' (a :: lg) ∧ rpo b a') →
rpo_mul l' l.
Lemma rpo_lex_same_length :
∀ l l', rpo_lex l l' → length l = length l'.
Lemma rpo_subterm :
∀ s t, rpo t s → ∀ tj, direct_subterm tj t → rpo tj s.
Lemma rpo_closure :
∀ s t u,
(rpo t s → rpo u t → rpo u s) ∧
(rpo s t → rpo t s → False) ∧
(rpo s s → False) ∧
(rpo_eq s t → rpo_eq t s → s = t).
Lemma rpo_trans : ∀ s t u, rpo t s → rpo u t → rpo u s.
Record SN_term : Set :=
mk_sn
{
tt : term;
sn : Acc rpo tt
}.
Well-foundedness of rpo.
How to build a built a list of pairs (terms, proof of accessibility) from a global of accessibility on the list.
Projection on the first element of the pairs after building the
pairs as above is the identity.
Lemma projection_list_of_SN_terms :
∀ l proof, map tt (build_list_of_SN_terms l proof) = l.
Lemma in_sn_sn :
∀ l s, In s (map tt l) → Acc rpo s.
Definition of rpo on accessible terms.
Extension of rpo_lex to the accessible terms.
Inductive rpo_lex_rest : list SN_term → list SN_term → Prop :=
| List_gt_rest :
∀ s t l l', rpo_rest s t → length l = length l' →
rpo_lex_rest (s :: l) (t :: l')
| List_eq_rest : ∀ s t l l', tt s = tt t → rpo_lex_rest l l' →
rpo_lex_rest (s :: l) (t :: l').
A triviality: rpo on accessible terms is well-founded.
Lemma wf_on_rest : well_founded rpo_rest.
Lemma rpo_lex_rest_same_length :
∀ l l', rpo_lex_rest l l' → length l = length l'.
Lemma rpo_lex_rest_same_length :
∀ l l', rpo_lex_rest l l' → length l = length l'.
Proof of accessibility does not actually matter, provided at
least one exists.
Lemma acc_lex_drop_proof :
∀ s t l, tt s = tt t → Acc rpo_lex_rest (s::l) → Acc rpo_lex_rest (t::l).
Lexicographic extension of rpo on accessible terms lists is well-founded.
Extension of rpo_mul to the accessible terms.
Inductive rpo_mul_rest : list SN_term → list SN_term → Prop :=
| List_mul_rest :
∀ a lg ls lc l l',
list_permut (map tt l') (map tt (ls ++ lc)) →
list_permut (map tt l) (map tt (a :: lg ++ lc)) →
(∀ b, In b ls → ∃ a', In a' (a :: lg) ∧ rpo_rest b a') →
rpo_mul_rest l' l.
Definition of a finer grain for multiset extension.
Inductive rpo_mul_rest_step : list SN_term → list SN_term → Prop :=
| List_mul_rest_step :
∀ a ls lc l l',
list_permut (map tt l') (map tt (ls ++ lc)) →
list_permut (map tt l) (map tt (a :: lc)) →
(∀ b, In b ls → rpo_rest b a) →
rpo_mul_rest_step l' l.
The plain multiset extension is in the transitive closure of
the finer grain extension.
Splitting in two disjoint cases.
Lemma two_cases_rpo :
∀ a m n,
rpo_mul_rest_step n (a :: m) →
(∃ n', list_permut (map tt n) (map tt (a :: n')) ∧
rpo_mul_rest_step n' m) ∨
(∃ k, (∀ b, In b k → rpo_rest b a) ∧
list_permut (map tt n) (map tt (k ++ m))).
Lemma list_permut_map_acc :
∀ l l', list_permut (map tt l) (map tt l') →
Acc rpo_mul_rest_step l → Acc rpo_mul_rest_step l'.
Multiset extension of rpo on accessible terms lists is well-founded.
Another definition of rpo, only on scheme of accessible terms.
Definition rpo_term : relation (symbol × list SN_term) :=
fun f_l g_l' ⇒
match f_l with
| (f,l) ⇒
match g_l' with
| (g,l') ⇒
if F.eq_symbol_dec f g
then
match status f with
| Lex ⇒ rpo_lex_rest l l'
| Mul ⇒ rpo_mul_rest l l'
end
else prec f g
end
end.
Lemma wf_rpo_term : well_founded prec → well_founded rpo_term.
Lemma acc_build :
well_founded prec → ∀ f l,
Acc rpo (Term f (map (fun sn_tt ⇒ tt sn_tt) l)).