File FixpointReasoning
From MatchingLogic Require Export monotonic
DerivedOperators_Semantics.
Import MatchingLogic.Syntax.Notations.
Import MatchingLogic.Substitution.Notations.
Import MatchingLogic.DerivedOperators_Syntax.Notations.
Section with_signature.
Context {Σ : Signature}.
Open Scope ml_scope.
Lemma eval_mu_lfp_fixpoint M ρ ϕ :
well_formed_positive (patt_mu ϕ) →
let X := fresh_svar ϕ in
let F := Fassoc ρ (ϕ^{svar: 0 ↦ X}) X in
let Sfix := @eval Σ M ρ (patt_mu ϕ) in
F Sfix = Sfix.
Lemma eval_mu_lfp_least M ρ ϕ S:
well_formed_positive (patt_mu ϕ) →
let X := fresh_svar ϕ in
let F := Fassoc ρ (ϕ^{svar: 0 ↦ X}) X in
let Sfix := @eval Σ M ρ (patt_mu ϕ) in
(F S) ⊆ S →
Sfix ⊆ S.
Lemma eval_mu_if_lfp M ρ ϕ Sfix :
well_formed_positive (patt_mu ϕ) →
let X := fresh_svar ϕ in
let F := Fassoc ρ (ϕ^{svar: 0 ↦ X}) X in
(F Sfix) ⊆ Sfix →
(∀ S, (F S) ⊆ S → Sfix ⊆ S) →
Sfix = @eval Σ M ρ (patt_mu ϕ).
Lemma eval_mu_lfp_iff M ρ ϕ Sfix :
well_formed_positive (patt_mu ϕ) →
let X := fresh_svar ϕ in
let F := Fassoc ρ (ϕ^{svar: 0 ↦ X}) X in
(
(F Sfix) ⊆ Sfix ∧
(∀ S, (F S) ⊆ S → Sfix ⊆ S)
) ↔ Sfix = @eval Σ M ρ (patt_mu ϕ).
(* mu X. base \/ step X *)
(* Nats = mu X. 0 \/ succ X *)
(* Nats = { x | \ex x_0,x_1,..x_n . x_0 \in 0 /\ x_{i+1} \in succ x_i /\ x = x_n } *)
(* 0, 1, 2,... x*)
Section inductive_generation.
Context (base step : Pattern).
Let patt_ind_gen_body := (patt_or (nest_mu base) (patt_app (nest_mu step) (patt_bound_svar 0))).
(* Let patt_ind_gen_simple_body := (patt_or base (patt_app step (patt_free_svar (fresh_svar patt_ind_gen_body)))). *)
Definition patt_ind_gen := patt_mu patt_ind_gen_body.
Hypothesis (Hwfpbase : well_formed_positive base).
Hypothesis (Hwfpstep : well_formed_positive step).
Lemma patt_ind_gen_wfp:
well_formed_positive patt_ind_gen.
Lemma svar_open_patt_ind_gen_body_simpl M ρ X:
svar_is_fresh_in X patt_ind_gen_body →
@eval Σ M ρ (patt_ind_gen_body^{svar: 0 ↦ X})
= @eval Σ M ρ (patt_or base (patt_app step (patt_free_svar X))).
Section with_eval.
Context (M : @Model Σ).
Context (ρ : @Valuation Σ M).
Let F := let X := fresh_svar patt_ind_gen_body in
@Fassoc Σ M ρ (patt_ind_gen_body^{svar: 0 ↦ X}) X.
(*
Lemma svar_open_patt_ind_gen_body_assoc S:
let X := fresh_svar patt_ind_gen_body in
eval ρₑ (update_svar_val X S ρₛ) (svar_open 0 X patt_ind_gen_body)
= F S.
Proof. reflexivity.
(*
cbv zeta.
rewrite svar_open_patt_ind_gen_body_simpl.
{ apply set_svar_fresh_is_fresh. }
subst F. unfold Fassoc.
rewrite svar_open_patt_ind_gen_body_simpl.
{ apply set_svar_fresh_is_fresh. }
reflexivity.*)
Qed.
*)
(* I can imagine this lemma to be proven automatically. *)
Lemma F_interp: F = λ A, (eval ρ base)
∪ (app_ext (eval ρ step) A).
Definition is_witnessing_sequence_old (m : Domain M) (l : list (Domain M)) :=
(last l = Some m) ∧
(match l with
| [] ⇒ False
| m₀::ms ⇒ (m₀ ∈ @eval Σ M ρ base)
∧ (@Forall _
(λ (x : (Domain M) × (Domain M)),
let (old, new) := x in
new ∈
app_ext
(@eval Σ M ρ step)
{[ old ]}
)
(zip (m₀::ms) ms)
)
end).
(* This sequence is the reversed version from the informal introduction in line 139
For example, for Nat model elements, the witnessing sequence for 5 is 5,4,3,2,1,0 *)
Definition is_witnessing_sequence (m : Domain M) (l : list (Domain M)) :=
(∃ lst, last l = Some lst ∧ lst ∈ @eval Σ M ρ base)
∧
hd_error l = Some m
∧
((@Forall _ (uncurry (λ new old,
new ∈
app_ext
(@eval Σ M ρ step)
{[old]}
))
(zip l (tail l))
)).
(* If we have a witnessing sequence x₁ x₂ ... xₙ xₙ₊₁ ... xlast
and xₙ matches `base`, then xₙ xₙ₊₁ is a witnessing sequence, too.
*)
Lemma witnessing_sequence_middle (m : Domain M) (l : list (Domain M)) (n : nat) (m' : Domain M) :
is_witnessing_sequence m l →
l !! n = Some m' →
is_witnessing_sequence m' (drop n l).
(* TODO: refactor, because this is a corollary of 'witnessing_sequence_middle'
by using n = 1 *)
Lemma witnessing_sequence_tail (m : Domain M) (l : list (Domain M)) (m' : Domain M) :
is_witnessing_sequence m l →
head (tail l) = Some m' →
is_witnessing_sequence m' (tail l).
Lemma is_witnessing_sequence_iff_is_witnessing_sequence_old_reverse (m : Domain M) (l : list (Domain M)) :
is_witnessing_sequence m l ↔ is_witnessing_sequence_old m (reverse l).
Lemma witnessing_sequence_extend (m m' : Domain M) (l : list (Domain M)) :
(is_witnessing_sequence m l
∧ (∃ step', step' ∈ eval ρ step ∧ m' ∈ app_interp _ step' m)
(* TODO: would this be easier to use/prove/understand to
have `m' ∈ app_ext (eval ρ step) {m}` instead? *)
) ↔ (is_witnessing_sequence m' (m'::l) ∧ l ≠ []).
Lemma witnessing_sequence_old_extend
(m x m' : Domain M) (l : list (Domain M)):
(is_witnessing_sequence_old m (x::l) ∧
∃ step', (step' ∈ eval ρ step ∧
m' ∈ app_interp _ step' m)) ↔
(last (x::l) = Some m ∧ is_witnessing_sequence_old m' ((x::l) ++ [m'])).
Definition witnessed_elements_old : propset (Domain M) :=
PropSet (λ m, ∃ l, is_witnessing_sequence_old m l).
Lemma witnessed_elements_old_prefixpoint : (F witnessed_elements_old) ⊆ witnessed_elements_old.
Lemma interp_included_in_witnessed_elements_old:
(@eval Σ M ρ patt_ind_gen) ⊆ witnessed_elements_old.
Lemma eval_patt_ind_gen_fix :
let Sfix := eval ρ patt_ind_gen in
F Sfix = Sfix.
Definition witnessed_elements_old_of_max_len len : propset (Domain M) :=
PropSet (λ m, ∃ l, is_witnessing_sequence_old m l ∧ length l ≤ len).
(* TODO: S len is needed? There is no elements that have an empty
witnessing sequence. *)
Lemma witnessed_elements_old_of_max_len_included_in_interp len:
(witnessed_elements_old_of_max_len (S len)) ⊆ (@eval Σ M ρ patt_ind_gen).
Lemma witnessed_elements_old_included_in_interp:
witnessed_elements_old ⊆ (@eval Σ M ρ patt_ind_gen).
Definition witnessed_elements : propset (Domain M) :=
PropSet (λ m, ∃ l, is_witnessing_sequence m l).
Lemma witnessed_elements_old_eq_witnessed_elements :
witnessed_elements_old = witnessed_elements.
Lemma patt_ind_gen_simpl:
@eval Σ M ρ patt_ind_gen = witnessed_elements.
Section injective.
Hypothesis (Domain_eq_dec : EqDecision (Domain M)).
Hypothesis (Hstep_total_function : @is_total_function _ M step witnessed_elements witnessed_elements ρ).
Hypothesis (Hstep_injective : @total_function_is_injective _ M step witnessed_elements ρ).
Hypothesis (Hbase_step_no_confusion
: (eval ρ base)
∩ (app_ext (eval ρ step) witnessed_elements) = ∅).
Lemma witnessed_elements_unique_seq :
∀ m l₁ l₂, is_witnessing_sequence m l₁ → is_witnessing_sequence m l₂ → l₁ = l₂.
End injective.
End with_eval.
End inductive_generation.
End with_signature.
DerivedOperators_Semantics.
Import MatchingLogic.Syntax.Notations.
Import MatchingLogic.Substitution.Notations.
Import MatchingLogic.DerivedOperators_Syntax.Notations.
Section with_signature.
Context {Σ : Signature}.
Open Scope ml_scope.
Lemma eval_mu_lfp_fixpoint M ρ ϕ :
well_formed_positive (patt_mu ϕ) →
let X := fresh_svar ϕ in
let F := Fassoc ρ (ϕ^{svar: 0 ↦ X}) X in
let Sfix := @eval Σ M ρ (patt_mu ϕ) in
F Sfix = Sfix.
Lemma eval_mu_lfp_least M ρ ϕ S:
well_formed_positive (patt_mu ϕ) →
let X := fresh_svar ϕ in
let F := Fassoc ρ (ϕ^{svar: 0 ↦ X}) X in
let Sfix := @eval Σ M ρ (patt_mu ϕ) in
(F S) ⊆ S →
Sfix ⊆ S.
Lemma eval_mu_if_lfp M ρ ϕ Sfix :
well_formed_positive (patt_mu ϕ) →
let X := fresh_svar ϕ in
let F := Fassoc ρ (ϕ^{svar: 0 ↦ X}) X in
(F Sfix) ⊆ Sfix →
(∀ S, (F S) ⊆ S → Sfix ⊆ S) →
Sfix = @eval Σ M ρ (patt_mu ϕ).
Lemma eval_mu_lfp_iff M ρ ϕ Sfix :
well_formed_positive (patt_mu ϕ) →
let X := fresh_svar ϕ in
let F := Fassoc ρ (ϕ^{svar: 0 ↦ X}) X in
(
(F Sfix) ⊆ Sfix ∧
(∀ S, (F S) ⊆ S → Sfix ⊆ S)
) ↔ Sfix = @eval Σ M ρ (patt_mu ϕ).
(* mu X. base \/ step X *)
(* Nats = mu X. 0 \/ succ X *)
(* Nats = { x | \ex x_0,x_1,..x_n . x_0 \in 0 /\ x_{i+1} \in succ x_i /\ x = x_n } *)
(* 0, 1, 2,... x*)
Section inductive_generation.
Context (base step : Pattern).
Let patt_ind_gen_body := (patt_or (nest_mu base) (patt_app (nest_mu step) (patt_bound_svar 0))).
(* Let patt_ind_gen_simple_body := (patt_or base (patt_app step (patt_free_svar (fresh_svar patt_ind_gen_body)))). *)
Definition patt_ind_gen := patt_mu patt_ind_gen_body.
Hypothesis (Hwfpbase : well_formed_positive base).
Hypothesis (Hwfpstep : well_formed_positive step).
Lemma patt_ind_gen_wfp:
well_formed_positive patt_ind_gen.
Lemma svar_open_patt_ind_gen_body_simpl M ρ X:
svar_is_fresh_in X patt_ind_gen_body →
@eval Σ M ρ (patt_ind_gen_body^{svar: 0 ↦ X})
= @eval Σ M ρ (patt_or base (patt_app step (patt_free_svar X))).
Section with_eval.
Context (M : @Model Σ).
Context (ρ : @Valuation Σ M).
Let F := let X := fresh_svar patt_ind_gen_body in
@Fassoc Σ M ρ (patt_ind_gen_body^{svar: 0 ↦ X}) X.
(*
Lemma svar_open_patt_ind_gen_body_assoc S:
let X := fresh_svar patt_ind_gen_body in
eval ρₑ (update_svar_val X S ρₛ) (svar_open 0 X patt_ind_gen_body)
= F S.
Proof. reflexivity.
(*
cbv zeta.
rewrite svar_open_patt_ind_gen_body_simpl.
{ apply set_svar_fresh_is_fresh. }
subst F. unfold Fassoc.
rewrite svar_open_patt_ind_gen_body_simpl.
{ apply set_svar_fresh_is_fresh. }
reflexivity.*)
Qed.
*)
(* I can imagine this lemma to be proven automatically. *)
Lemma F_interp: F = λ A, (eval ρ base)
∪ (app_ext (eval ρ step) A).
Definition is_witnessing_sequence_old (m : Domain M) (l : list (Domain M)) :=
(last l = Some m) ∧
(match l with
| [] ⇒ False
| m₀::ms ⇒ (m₀ ∈ @eval Σ M ρ base)
∧ (@Forall _
(λ (x : (Domain M) × (Domain M)),
let (old, new) := x in
new ∈
app_ext
(@eval Σ M ρ step)
{[ old ]}
)
(zip (m₀::ms) ms)
)
end).
(* This sequence is the reversed version from the informal introduction in line 139
For example, for Nat model elements, the witnessing sequence for 5 is 5,4,3,2,1,0 *)
Definition is_witnessing_sequence (m : Domain M) (l : list (Domain M)) :=
(∃ lst, last l = Some lst ∧ lst ∈ @eval Σ M ρ base)
∧
hd_error l = Some m
∧
((@Forall _ (uncurry (λ new old,
new ∈
app_ext
(@eval Σ M ρ step)
{[old]}
))
(zip l (tail l))
)).
(* If we have a witnessing sequence x₁ x₂ ... xₙ xₙ₊₁ ... xlast
and xₙ matches `base`, then xₙ xₙ₊₁ is a witnessing sequence, too.
*)
Lemma witnessing_sequence_middle (m : Domain M) (l : list (Domain M)) (n : nat) (m' : Domain M) :
is_witnessing_sequence m l →
l !! n = Some m' →
is_witnessing_sequence m' (drop n l).
(* TODO: refactor, because this is a corollary of 'witnessing_sequence_middle'
by using n = 1 *)
Lemma witnessing_sequence_tail (m : Domain M) (l : list (Domain M)) (m' : Domain M) :
is_witnessing_sequence m l →
head (tail l) = Some m' →
is_witnessing_sequence m' (tail l).
Lemma is_witnessing_sequence_iff_is_witnessing_sequence_old_reverse (m : Domain M) (l : list (Domain M)) :
is_witnessing_sequence m l ↔ is_witnessing_sequence_old m (reverse l).
Lemma witnessing_sequence_extend (m m' : Domain M) (l : list (Domain M)) :
(is_witnessing_sequence m l
∧ (∃ step', step' ∈ eval ρ step ∧ m' ∈ app_interp _ step' m)
(* TODO: would this be easier to use/prove/understand to
have `m' ∈ app_ext (eval ρ step) {m}` instead? *)
) ↔ (is_witnessing_sequence m' (m'::l) ∧ l ≠ []).
Lemma witnessing_sequence_old_extend
(m x m' : Domain M) (l : list (Domain M)):
(is_witnessing_sequence_old m (x::l) ∧
∃ step', (step' ∈ eval ρ step ∧
m' ∈ app_interp _ step' m)) ↔
(last (x::l) = Some m ∧ is_witnessing_sequence_old m' ((x::l) ++ [m'])).
Definition witnessed_elements_old : propset (Domain M) :=
PropSet (λ m, ∃ l, is_witnessing_sequence_old m l).
Lemma witnessed_elements_old_prefixpoint : (F witnessed_elements_old) ⊆ witnessed_elements_old.
Lemma interp_included_in_witnessed_elements_old:
(@eval Σ M ρ patt_ind_gen) ⊆ witnessed_elements_old.
Lemma eval_patt_ind_gen_fix :
let Sfix := eval ρ patt_ind_gen in
F Sfix = Sfix.
Definition witnessed_elements_old_of_max_len len : propset (Domain M) :=
PropSet (λ m, ∃ l, is_witnessing_sequence_old m l ∧ length l ≤ len).
(* TODO: S len is needed? There is no elements that have an empty
witnessing sequence. *)
Lemma witnessed_elements_old_of_max_len_included_in_interp len:
(witnessed_elements_old_of_max_len (S len)) ⊆ (@eval Σ M ρ patt_ind_gen).
Lemma witnessed_elements_old_included_in_interp:
witnessed_elements_old ⊆ (@eval Σ M ρ patt_ind_gen).
Definition witnessed_elements : propset (Domain M) :=
PropSet (λ m, ∃ l, is_witnessing_sequence m l).
Lemma witnessed_elements_old_eq_witnessed_elements :
witnessed_elements_old = witnessed_elements.
Lemma patt_ind_gen_simpl:
@eval Σ M ρ patt_ind_gen = witnessed_elements.
Section injective.
Hypothesis (Domain_eq_dec : EqDecision (Domain M)).
Hypothesis (Hstep_total_function : @is_total_function _ M step witnessed_elements witnessed_elements ρ).
Hypothesis (Hstep_injective : @total_function_is_injective _ M step witnessed_elements ρ).
Hypothesis (Hbase_step_no_confusion
: (eval ρ base)
∩ (app_ext (eval ρ step) witnessed_elements) = ∅).
Lemma witnessed_elements_unique_seq :
∀ m l₁ l₂, is_witnessing_sequence m l₁ → is_witnessing_sequence m l₂ → l₁ = l₂.
End injective.
End with_eval.
End inductive_generation.
End with_signature.
This page has been generated by coqdoc