Tableaux.Skolemization
From Tableaux Require Import Prelude.Core.
From Tableaux Require Import Syntax.
From Tableaux Require Import Semantics.
In this file, we specify Skolemization so that it can be used in a generic setting
in tableaux proofs. We give the data it must furnish, and the properties it must
follow. The goal is to be able to be Skolemization-independent in the definition of
tableaux and make it work seamlessly for different instances of this class.
Section SkolemizationDef.
Context {pred func var : Type} `{isAtom pred} `{isAtom func} `{isAtom var}.
Let set_var := set_atom var.
Let set_func := set_atom func.
Let Term := Term func var.
Let Form := Form pred func var.
Let Ctx := list Form.
Context {pred func var : Type} `{isAtom pred} `{isAtom func} `{isAtom var}.
Let set_var := set_atom var.
Let set_func := set_atom func.
Let Term := Term func var.
Let Form := Form pred func var.
Let Ctx := list Form.
We start by defining skolemization "records", which vary depending on the skolemization.
For instance, starting from pre-inner Skolemization, we want to check that each function
symbol generated by skolemizing the same formula is the same, so we need a kind of
key-value map.
For e.g., outer and inner Skolemization, we don't need a record, so it will simply be
instantiated to unit.
Section SkoRecord.
Record SkoRecordData :=
{ record :> Type
; record_eqb :: EqBool record
; to_set : record -> set_func
; value_record : func -> record -> option Form
; join : record -> record -> record
; single_record : func -> Form -> record
; empty_record : record }.
#[global] Arguments value_record {_} _ _.
#[global] Arguments to_set {_} _.
#[global] Arguments join {_} _ _.
#[global] Arguments empty_record {_}.
Section SkoRecordDataDefs.
Context {RecordData : SkoRecordData}.
Definition in_record (f : func) (r : RecordData) : Prop :=
match value_record f r with
| None => False
| Some _ => True
end.
Definition mem_record (f : func) (r : RecordData) : bool :=
match value_record f r with
| None => false
| Some _ => true
end.
Lemma mem_record_spec :
forall (f : func) (r : RecordData),
mem_record f r = true <-> in_record f r.
Proof using Type.
intros. rewrite /mem_record /in_record.
destruct (value_record f r).
- tauto.
- easy.
Qed.
End SkoRecordDataDefs.
Class SkoRecordSpecs (RecordData : SkoRecordData) :=
{ record_ext :
forall (r1 r2 : RecordData),
r1 = r2 <->
(forall (f : func), in_record f r1 <-> in_record f r2)
; single_spec :
forall (f g : func) (F : Form),
in_record g (single_record RecordData f F) -> g = f
; join_spec :
forall (f : func) (r1 r2 : RecordData),
in_record f (join r1 r2) <-> in_record f r1 \/ in_record f r2
; value_record_spec1 :
forall (f : func), @value_record RecordData f empty_record = None
; join_to_set :
forall (r1 r2 : RecordData),
to_set (join r1 r2) = to_set r1 \union to_set r2
; single_to_set :
forall (f : func) (F : Form),
to_set (single_record RecordData f F) = singleton f
; empty_to_set : @to_set RecordData empty_record = \{\} }.
Record SkoRecord :=
{ data :> SkoRecordData
; specs :: SkoRecordSpecs data }.
End SkoRecord.
Record SkoRecordData :=
{ record :> Type
; record_eqb :: EqBool record
; to_set : record -> set_func
; value_record : func -> record -> option Form
; join : record -> record -> record
; single_record : func -> Form -> record
; empty_record : record }.
#[global] Arguments value_record {_} _ _.
#[global] Arguments to_set {_} _.
#[global] Arguments join {_} _ _.
#[global] Arguments empty_record {_}.
Section SkoRecordDataDefs.
Context {RecordData : SkoRecordData}.
Definition in_record (f : func) (r : RecordData) : Prop :=
match value_record f r with
| None => False
| Some _ => True
end.
Definition mem_record (f : func) (r : RecordData) : bool :=
match value_record f r with
| None => false
| Some _ => true
end.
Lemma mem_record_spec :
forall (f : func) (r : RecordData),
mem_record f r = true <-> in_record f r.
Proof using Type.
intros. rewrite /mem_record /in_record.
destruct (value_record f r).
- tauto.
- easy.
Qed.
End SkoRecordDataDefs.
Class SkoRecordSpecs (RecordData : SkoRecordData) :=
{ record_ext :
forall (r1 r2 : RecordData),
r1 = r2 <->
(forall (f : func), in_record f r1 <-> in_record f r2)
; single_spec :
forall (f g : func) (F : Form),
in_record g (single_record RecordData f F) -> g = f
; join_spec :
forall (f : func) (r1 r2 : RecordData),
in_record f (join r1 r2) <-> in_record f r1 \/ in_record f r2
; value_record_spec1 :
forall (f : func), @value_record RecordData f empty_record = None
; join_to_set :
forall (r1 r2 : RecordData),
to_set (join r1 r2) = to_set r1 \union to_set r2
; single_to_set :
forall (f : func) (F : Form),
to_set (single_record RecordData f F) = singleton f
; empty_to_set : @to_set RecordData empty_record = \{\} }.
Record SkoRecord :=
{ data :> SkoRecordData
; specs :: SkoRecordSpecs data }.
End SkoRecord.
We define the first part of the Skolemization process: the data. It takes:
- a Skolemization record,
- a boolean predicate is_sko, to check if a given term is a valid skolemization w.r.t. (i) the formula which is Skolemized, (ii) the Skolemization context, (iii) the set of free variables of the current branch, and (iv) the set of function symbols of the tableau,
- a symbol function, that should always return a func if the term t is a skolemization,
- and an args function, that should always return the arguments of the term t if it is a Skolemization.
Record SkolemizationData :=
{ sko_record : SkoRecord
; is_sko :> Term -> Form -> sko_record -> set_var -> set_func -> bool
; symbol :
forall {t : Term} {F : Form} {symbs : sko_record} {fvs : set_var} {func_symbols : set_func},
is_sko t F symbs fvs func_symbols = true -> func
; args :
forall {t : Term} {F : Form} {symbs : sko_record} {fvs : set_var} {func_symbols : set_func},
is_sko t F symbs fvs func_symbols = true -> list Term }.
Class isSkolemization (data : SkolemizationData) :=
{ is_func :
forall {t : Term} {F : Form} {symbs : sko_record data} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko data t F symbs fvs func_symbols = true),
t = Fun (symbol data hsko) (args data hsko)
; args_sound :
forall {t : Term} {F : Form} {symbs : sko_record data} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko data t F symbs fvs func_symbols = true) (t : Term),
List.In t (args data hsko) -> exists (x : var), t = Free x
; is_sko_consistent :
forall {t : Term} {F : Form} {symbs : sko_record data} {fvs : set_var}
{func_symbols func_symbols' : set_func},
func_symbols \subseteq func_symbols' ->
is_sko data t F symbs fvs func_symbols' = true ->
is_sko data t F symbs fvs func_symbols = true
; is_sko_sound :
forall {t : Term} {F : Form} {symbs : sko_record data} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko data t (Neg (All F)) symbs fvs func_symbols = true) (M : Model pred func),
exists (f : func -> list M -> M),
(forall (mu : env M var),
subset (function_symbols F) func_symbols ->
[[ M # [] # mu '|= Neg (All F) ]] ->
[[ ReplacementModel M f # [] # mu '|= Neg F{0 \to t} ]]) /\
(forall (F : Form) (mu : env M var),
subset (function_symbols F) func_symbols -> [[ M # [] # mu '|= F ]] ->
[[ ReplacementModel M f # [] # mu '|= F ]]) }.
Record Skolemization_ :=
{ skoData :> SkolemizationData
; is_skolemization :: isSkolemization skoData }.
End SkolemizationDef.
Coercion specs : SkoRecord >-> SkoRecordSpecs.
Coercion is_skolemization : Skolemization_ >-> isSkolemization.
Arguments SkoRecordData _ _ _ {_ _ _}.
Arguments SkoRecord _ _ _ {_ _ _}.
Arguments SkolemizationData _ _ _ {_ _ _}.
Arguments Skolemization_ _ _ _ {_ _ _}.
Arguments sko_record {_ _ _ _ _ _} _.
Section SkoSymbolLemmas.
Context {pred func var : Type} `{isAtom pred} `{isAtom func} `{isAtom var}
{record : SkoRecord pred func var}.
Let Term := Term func var.
Let Form := Form pred func var.
Definition add_symbol (f : func) (F : Form) (r : record) : record :=
join (single_record record f F) r.
Lemma join_unitr :
forall (r : record),
join r empty_record = r.
Proof using Type.
intro; rewrite record_ext; intros f; split.
- rewrite join_spec; intros [h | contra]; auto.
unfold in_record in contra. now rewrite value_record_spec1 in contra.
- rewrite join_spec; intros h; auto.
Qed.
Lemma join_unitl :
forall (r : record),
join empty_record r = r.
Proof using Type.
intro; rewrite record_ext; intros f; split.
- rewrite join_spec; intros [contra | h]; auto.
unfold in_record in contra. now rewrite value_record_spec1 in contra.
- rewrite join_spec; intros h; auto.
Qed.
End SkoSymbolLemmas.
Section SkoDefs.
Context {pred func var : Type} `{isAtom pred} `{isAtom func} `{isAtom var}
(sko : Skolemization_ pred func var).
Let Term := Term func var.
Let Form := Form pred func var.
Let set_var := set_atom var.
Let set_func := set_atom func.
Lemma symbol_sound :
forall {t : Term} {F : Form} {symbs : sko_record sko} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko sko t F symbs fvs func_symbols = true),
get_symbol t = Some (symbol sko hsko).
Proof using Type.
intros. etransitivity. {
apply f_equal. exact (is_func hsko).
} now cbn.
Qed.
Lemma sko_function_symbols_args :
forall {t : Term} {F : Form} {symbs : sko_record sko} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko sko t F symbs fvs func_symbols = true),
function_symbols (args sko hsko) = \{\}.
Proof using pred.
intros. have h := is_func hsko. specialize (h sko).
destruct t; try easy. injection h => <- _.
have hfree := args_sound hsko.
specialize (hfree sko). injection h => el _.
have hfree' : forall t : Syntax.Term func var, List.In t l -> exists x : var, t = Free x.
{ intros; apply hfree. now destruct el. }
clear hfree el h hsko func_symbols fvs symbs F f.
induction l as [|v vs IHvs]; auto.
cbn; rewrite set_fold_left empty_unitl -IHvs.
- intros; apply hfree'. now right.
- apply set_ext; intros g; split; intros hin.
+ rewrite union_spec in hin; destruct hin as [contra | hvs]; auto.
* have [x e] : exists x : var, v = Free x.
{ apply hfree'. now left. }
rewrite e in contra; cbn in contra.
now apply empty_spec in contra.
* rewrite set_fold_left union_spec in hvs; destruct hvs; auto.
+ rewrite union_spec. right. rewrite set_fold_left union_spec.
now left.
Qed.
Lemma sko_function_symbols_sound :
forall {t : Term} {F : Form} {symbs : sko_record sko} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko sko t F symbs fvs func_symbols = true),
function_symbols t = singleton (symbol sko hsko).
Proof using pred.
intros ??????. etransitivity. {
apply f_equal. exact (is_func hsko).
} cbn. rewrite set_fold_left; apply set_ext; intros f; split; intros hin.
- rewrite union_spec in hin; destruct hin as [hsingl | contra]; auto.
have h := sko_function_symbols_args hsko.
have e :
(fold_left (fun (s : set_atom func) (b : Syntax.Term func var) => s \union function_symbols b)
(args sko hsko) \{ \}) =
function_symbols (args sko hsko).
{ reflexivity. }
rewrite e h in contra. now apply empty_spec in contra.
- rewrite union_spec; now left.
Qed.
End SkoDefs.
{ sko_record : SkoRecord
; is_sko :> Term -> Form -> sko_record -> set_var -> set_func -> bool
; symbol :
forall {t : Term} {F : Form} {symbs : sko_record} {fvs : set_var} {func_symbols : set_func},
is_sko t F symbs fvs func_symbols = true -> func
; args :
forall {t : Term} {F : Form} {symbs : sko_record} {fvs : set_var} {func_symbols : set_func},
is_sko t F symbs fvs func_symbols = true -> list Term }.
Class isSkolemization (data : SkolemizationData) :=
{ is_func :
forall {t : Term} {F : Form} {symbs : sko_record data} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko data t F symbs fvs func_symbols = true),
t = Fun (symbol data hsko) (args data hsko)
; args_sound :
forall {t : Term} {F : Form} {symbs : sko_record data} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko data t F symbs fvs func_symbols = true) (t : Term),
List.In t (args data hsko) -> exists (x : var), t = Free x
; is_sko_consistent :
forall {t : Term} {F : Form} {symbs : sko_record data} {fvs : set_var}
{func_symbols func_symbols' : set_func},
func_symbols \subseteq func_symbols' ->
is_sko data t F symbs fvs func_symbols' = true ->
is_sko data t F symbs fvs func_symbols = true
; is_sko_sound :
forall {t : Term} {F : Form} {symbs : sko_record data} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko data t (Neg (All F)) symbs fvs func_symbols = true) (M : Model pred func),
exists (f : func -> list M -> M),
(forall (mu : env M var),
subset (function_symbols F) func_symbols ->
[[ M # [] # mu '|= Neg (All F) ]] ->
[[ ReplacementModel M f # [] # mu '|= Neg F{0 \to t} ]]) /\
(forall (F : Form) (mu : env M var),
subset (function_symbols F) func_symbols -> [[ M # [] # mu '|= F ]] ->
[[ ReplacementModel M f # [] # mu '|= F ]]) }.
Record Skolemization_ :=
{ skoData :> SkolemizationData
; is_skolemization :: isSkolemization skoData }.
End SkolemizationDef.
Coercion specs : SkoRecord >-> SkoRecordSpecs.
Coercion is_skolemization : Skolemization_ >-> isSkolemization.
Arguments SkoRecordData _ _ _ {_ _ _}.
Arguments SkoRecord _ _ _ {_ _ _}.
Arguments SkolemizationData _ _ _ {_ _ _}.
Arguments Skolemization_ _ _ _ {_ _ _}.
Arguments sko_record {_ _ _ _ _ _} _.
Section SkoSymbolLemmas.
Context {pred func var : Type} `{isAtom pred} `{isAtom func} `{isAtom var}
{record : SkoRecord pred func var}.
Let Term := Term func var.
Let Form := Form pred func var.
Definition add_symbol (f : func) (F : Form) (r : record) : record :=
join (single_record record f F) r.
Lemma join_unitr :
forall (r : record),
join r empty_record = r.
Proof using Type.
intro; rewrite record_ext; intros f; split.
- rewrite join_spec; intros [h | contra]; auto.
unfold in_record in contra. now rewrite value_record_spec1 in contra.
- rewrite join_spec; intros h; auto.
Qed.
Lemma join_unitl :
forall (r : record),
join empty_record r = r.
Proof using Type.
intro; rewrite record_ext; intros f; split.
- rewrite join_spec; intros [contra | h]; auto.
unfold in_record in contra. now rewrite value_record_spec1 in contra.
- rewrite join_spec; intros h; auto.
Qed.
End SkoSymbolLemmas.
Section SkoDefs.
Context {pred func var : Type} `{isAtom pred} `{isAtom func} `{isAtom var}
(sko : Skolemization_ pred func var).
Let Term := Term func var.
Let Form := Form pred func var.
Let set_var := set_atom var.
Let set_func := set_atom func.
Lemma symbol_sound :
forall {t : Term} {F : Form} {symbs : sko_record sko} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko sko t F symbs fvs func_symbols = true),
get_symbol t = Some (symbol sko hsko).
Proof using Type.
intros. etransitivity. {
apply f_equal. exact (is_func hsko).
} now cbn.
Qed.
Lemma sko_function_symbols_args :
forall {t : Term} {F : Form} {symbs : sko_record sko} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko sko t F symbs fvs func_symbols = true),
function_symbols (args sko hsko) = \{\}.
Proof using pred.
intros. have h := is_func hsko. specialize (h sko).
destruct t; try easy. injection h => <- _.
have hfree := args_sound hsko.
specialize (hfree sko). injection h => el _.
have hfree' : forall t : Syntax.Term func var, List.In t l -> exists x : var, t = Free x.
{ intros; apply hfree. now destruct el. }
clear hfree el h hsko func_symbols fvs symbs F f.
induction l as [|v vs IHvs]; auto.
cbn; rewrite set_fold_left empty_unitl -IHvs.
- intros; apply hfree'. now right.
- apply set_ext; intros g; split; intros hin.
+ rewrite union_spec in hin; destruct hin as [contra | hvs]; auto.
* have [x e] : exists x : var, v = Free x.
{ apply hfree'. now left. }
rewrite e in contra; cbn in contra.
now apply empty_spec in contra.
* rewrite set_fold_left union_spec in hvs; destruct hvs; auto.
+ rewrite union_spec. right. rewrite set_fold_left union_spec.
now left.
Qed.
Lemma sko_function_symbols_sound :
forall {t : Term} {F : Form} {symbs : sko_record sko} {fvs : set_var} {func_symbols : set_func}
(hsko : is_sko sko t F symbs fvs func_symbols = true),
function_symbols t = singleton (symbol sko hsko).
Proof using pred.
intros ??????. etransitivity. {
apply f_equal. exact (is_func hsko).
} cbn. rewrite set_fold_left; apply set_ext; intros f; split; intros hin.
- rewrite union_spec in hin; destruct hin as [hsingl | contra]; auto.
have h := sko_function_symbols_args hsko.
have e :
(fold_left (fun (s : set_atom func) (b : Syntax.Term func var) => s \union function_symbols b)
(args sko hsko) \{ \}) =
function_symbols (args sko hsko).
{ reflexivity. }
rewrite e h in contra. now apply empty_spec in contra.
- rewrite union_spec; now left.
Qed.
End SkoDefs.
Section SkolemizationInstances.
Context {pred func var : Type} `{isAtom pred} `{isAtom func} `{isAtom var} `{set_nat : set nat}.
Let set_var := set_atom var.
Let set_func := set_atom func.
Let Term := Term func var.
Let Form := Form pred func var.
Let Ctx := list Form.
Existing Instance set_func.
Context {pred func var : Type} `{isAtom pred} `{isAtom func} `{isAtom var} `{set_nat : set nat}.
Let set_var := set_atom var.
Let set_func := set_atom func.
Let Term := Term func var.
Let Form := Form pred func var.
Let Ctx := list Form.
Existing Instance set_func.
Definition SkoRecordData_set :
SkoRecordData pred func var.
Proof.
unshelve econstructor.
- exact set_func.
- typeclasses eauto.
- exact (fun s => s).
- exact (fun f s => if mem f s then Some Bot else None).
- exact union.
- exact (fun f _ => singleton f).
- exact \{\}.
Defined.
Lemma SkoRecordSpecs_set :
SkoRecordSpecs SkoRecordData_set.
Proof using Type.
constructor.
- intros; split; intro h; intros.
+ rewrite set_ext in h; specialize (h f).
unfold in_record; cbn in *.
destruct (mem f r1) eqn:hmem.
* rewrite mem_spec h -mem_spec in hmem.
rewrite hmem //.
* rewrite mem_spec' h -mem_spec' in hmem.
rewrite hmem //.
+ rewrite set_ext; intro f; specialize (h f).
unfold in_record in h; cbn in *.
destruct (mem f r1) eqn:hmem1, (mem f r2) eqn:hmem2.
* rewrite !mem_spec in hmem1, hmem2. split; auto.
* destruct h; easy.
* destruct h; easy.
* rewrite !mem_spec' in hmem1, hmem2. split; auto.
-- intro hr1; exfalso; now apply hmem1.
-- intro hr2; exfalso; now apply hmem2.
- intros f g F; unfold in_record; cbn.
destruct (mem g (singleton f)) eqn:eg; intro; try easy.
rewrite mem_spec singleton_spec // in eg |- *.
- intros f r1 r2; unfold in_record; cbn.
destruct (mem f (r1 \union r2)) eqn:eunion, (mem f r1) eqn:er1, (mem f r2) eqn:er2;
firstorder.
+ rewrite !mem_spec' in er1, er2.
rewrite mem_spec union_spec in eunion. exfalso; destruct eunion; auto.
+ rewrite !mem_spec in er1, er2.
rewrite mem_spec' union_spec in eunion. apply eunion; now left.
+ rewrite !mem_spec in er1, er2.
rewrite mem_spec' union_spec in eunion. apply eunion; now left.
+ rewrite mem_spec in er1; rewrite mem_spec' in er2.
rewrite mem_spec' union_spec in eunion. apply eunion; now left.
+ rewrite mem_spec' in er1; rewrite mem_spec in er2.
rewrite mem_spec' union_spec in eunion. apply eunion; now right.
- intro; cbn. destruct (mem f \{\}) eqn:eempty; auto.
rewrite mem_spec in eempty. exfalso; eapply empty_spec; eauto.
- intros ??; now cbn.
- reflexivity.
- reflexivity.
Qed.
Definition sko_record_set : SkoRecord pred func var.
Proof.
unshelve econstructor.
- exact SkoRecordData_set.
- exact SkoRecordSpecs_set.
Defined.
SkoRecordData pred func var.
Proof.
unshelve econstructor.
- exact set_func.
- typeclasses eauto.
- exact (fun s => s).
- exact (fun f s => if mem f s then Some Bot else None).
- exact union.
- exact (fun f _ => singleton f).
- exact \{\}.
Defined.
Lemma SkoRecordSpecs_set :
SkoRecordSpecs SkoRecordData_set.
Proof using Type.
constructor.
- intros; split; intro h; intros.
+ rewrite set_ext in h; specialize (h f).
unfold in_record; cbn in *.
destruct (mem f r1) eqn:hmem.
* rewrite mem_spec h -mem_spec in hmem.
rewrite hmem //.
* rewrite mem_spec' h -mem_spec' in hmem.
rewrite hmem //.
+ rewrite set_ext; intro f; specialize (h f).
unfold in_record in h; cbn in *.
destruct (mem f r1) eqn:hmem1, (mem f r2) eqn:hmem2.
* rewrite !mem_spec in hmem1, hmem2. split; auto.
* destruct h; easy.
* destruct h; easy.
* rewrite !mem_spec' in hmem1, hmem2. split; auto.
-- intro hr1; exfalso; now apply hmem1.
-- intro hr2; exfalso; now apply hmem2.
- intros f g F; unfold in_record; cbn.
destruct (mem g (singleton f)) eqn:eg; intro; try easy.
rewrite mem_spec singleton_spec // in eg |- *.
- intros f r1 r2; unfold in_record; cbn.
destruct (mem f (r1 \union r2)) eqn:eunion, (mem f r1) eqn:er1, (mem f r2) eqn:er2;
firstorder.
+ rewrite !mem_spec' in er1, er2.
rewrite mem_spec union_spec in eunion. exfalso; destruct eunion; auto.
+ rewrite !mem_spec in er1, er2.
rewrite mem_spec' union_spec in eunion. apply eunion; now left.
+ rewrite !mem_spec in er1, er2.
rewrite mem_spec' union_spec in eunion. apply eunion; now left.
+ rewrite mem_spec in er1; rewrite mem_spec' in er2.
rewrite mem_spec' union_spec in eunion. apply eunion; now left.
+ rewrite mem_spec' in er1; rewrite mem_spec in er2.
rewrite mem_spec' union_spec in eunion. apply eunion; now right.
- intro; cbn. destruct (mem f \{\}) eqn:eempty; auto.
rewrite mem_spec in eempty. exfalso; eapply empty_spec; eauto.
- intros ??; now cbn.
- reflexivity.
- reflexivity.
Qed.
Definition sko_record_set : SkoRecord pred func var.
Proof.
unshelve econstructor.
- exact SkoRecordData_set.
- exact SkoRecordSpecs_set.
Defined.
Generic definitions for different skolemizations
(* Use this function to avoid repeating the match on useless terms *)
Definition SkoWrapper_is_sko (t : Term) (P : func -> list Term -> bool) : bool :=
match t with
| Bound _ | Free _ => false
| Fun f l => P f l
end.
(* Use this function to get the skolem symbol (it abstracts away the impossible cases) *)
Definition SkoWrapper_symbol (t : Term) {P : func -> list Term -> bool}
(hsko : SkoWrapper_is_sko t P = true) : func.
refine
(match t as t0 return t = t0 -> func with
| Bound _ | Free _ => fun e => False_rect func _
| Fun f _ => fun _ => f
end eq_refl).
all: now rewrite e in hsko.
Defined.
Definition SkoWrapper_args (t : Term) {P : func -> list Term -> bool}
(hsko : SkoWrapper_is_sko t P = true) : list Term.
Proof.
refine
(match t as t0 return t = t0 -> list Term with
| Bound _ | Free _ => fun e => False_rect (list Term) _
| Fun _ l => fun _ => l
end eq_refl).
all: now rewrite e in hsko.
Defined.
Definition is_fv_in (S : set_atom var) (t : Term) : bool :=
match t with
| Bound _ | Fun _ _ => false
| Free x => mem x S
end.
Definition only_fv_in (S : set_atom var) (t : Term) : bool :=
match t with
| Bound _ | Free _ => false
| Fun f l => forallb (is_fv_in S) l
end.
Definition SkoWrapper_is_sko (t : Term) (P : func -> list Term -> bool) : bool :=
match t with
| Bound _ | Free _ => false
| Fun f l => P f l
end.
(* Use this function to get the skolem symbol (it abstracts away the impossible cases) *)
Definition SkoWrapper_symbol (t : Term) {P : func -> list Term -> bool}
(hsko : SkoWrapper_is_sko t P = true) : func.
refine
(match t as t0 return t = t0 -> func with
| Bound _ | Free _ => fun e => False_rect func _
| Fun f _ => fun _ => f
end eq_refl).
all: now rewrite e in hsko.
Defined.
Definition SkoWrapper_args (t : Term) {P : func -> list Term -> bool}
(hsko : SkoWrapper_is_sko t P = true) : list Term.
Proof.
refine
(match t as t0 return t = t0 -> list Term with
| Bound _ | Free _ => fun e => False_rect (list Term) _
| Fun _ l => fun _ => l
end eq_refl).
all: now rewrite e in hsko.
Defined.
Definition is_fv_in (S : set_atom var) (t : Term) : bool :=
match t with
| Bound _ | Fun _ _ => false
| Free x => mem x S
end.
Definition only_fv_in (S : set_atom var) (t : Term) : bool :=
match t with
| Bound _ | Free _ => false
| Fun f l => forallb (is_fv_in S) l
end.
In outer skolemization, we want to check that:
As the fact that it's a functorial term is already given by SkoWrapper_is_sko,
we focus on defining the other aspects here.
- t is a functorial term f (t1, ..., tn),
- such that f does not already appear in Gamma,
- and t1, ..., tn are actually all the free variables of (morally) the context.
Definition OuterSkolemization_is_sko_pred (F : Form) (fvs : set_var)
(func_symbols : set_func) (f : func) (l : list Term) : bool :=
negb (mem f func_symbols) && subsetb (fv F) fvs &&
eqb (fv l) fvs && forallb is_free l.
Lemma OuterSkolemization_is_sko_pred_sound :
forall (fvs : set_var) (func_symbols : set_func) (F : Form) (f : func) (l : list Term),
OuterSkolemization_is_sko_pred F fvs func_symbols f l = true ->
~(set_in f func_symbols) /\ fv F \subseteq fvs /\ fv l = fvs /\
(forall (t : Term), List.In t l -> exists (x : var), t = Free x).
Proof using Type.
intros ????? [ [ [hfresh%Bool.negb_true_iff hsub]%andb_prop e ]%andb_prop hfree ]%andb_prop;
repeat split.
- rewrite -mem_spec' //.
- now rewrite subsetb_spec in hsub.
- rewrite -eqbIsEq //.
- rewrite forallb_forall in hfree; intros ? hin; specialize (hfree t hin).
now apply is_free_sound in hfree.
Qed.
Definition OuterSkolemizationData : SkolemizationData pred func var.
Proof.
unshelve econstructor.
- exact sko_record_set.
(* in outer skolemization, we simply need to keep track of which symbols have been
instantiated *)
- intros t F _ fvs symbs2.
exact (SkoWrapper_is_sko t (OuterSkolemization_is_sko_pred F fvs symbs2)).
- intros t ???? hsko. apply (SkoWrapper_symbol t hsko).
- intros t ???? hsko. apply (SkoWrapper_args t hsko).
Defined.
Lemma OuterSkolemization_args_vars :
forall {func_symbols : set_func} {t : Term} {F : Form} {symbs : sko_record OuterSkolemizationData}
{fvs : set_var} (hsko : OuterSkolemizationData t F symbs fvs func_symbols = true),
exists (l : list var), args OuterSkolemizationData hsko =
map (fun v => Free v) l.
Proof using Type.
intros ??????. set largs := args OuterSkolemizationData hsko.
destruct t; try inversion hsko; cbn in hsko.
have eargs : largs = l by reflexivity. rewrite eargs.
have [ _ [ _ [ _ hargs ] ] ] := OuterSkolemization_is_sko_pred_sound _ _ _ _ _ H3.
clear largs eargs H3 hsko.
induction l as [|t ts IHts].
- now exists [].
- have ht := hargs t ltac:(now left).
destruct ht as (x & e).
have h : forall t, List.In t ts -> exists x : var, t = Free x.
{ intros; apply hargs. now right. }
specialize (IHts h). destruct IHts as (l0 & el0).
exists (x :: l0); cbn. rewrite e el0 //.
Qed.
Lemma OuterSkolemization_isLocallyClosed :
forall (t : Term) (F : Form) (symbs : sko_record OuterSkolemizationData) (fvs : set_var)
(func_symbols : set_func),
OuterSkolemizationData t F symbs fvs func_symbols = true -> isLocallyClosed t.
Proof using Type.
intros ????? hsko; destruct t; cbn in *; try (inversion hsko; fail).
apply OuterSkolemization_is_sko_pred_sound in hsko; destruct hsko as (_ & _ & _ & hfv).
clear func_symbols symbs F; induction l as [|t ts IHts]; unfold isLocallyClosed; cbn;
unfold is_empty; auto.
change (bv t \union bv_list ts = \{\}); apply is_empty_union; split.
+ have h : exists x, t = Free x by apply hfv; now left.
destruct h as (x & e); rewrite e; now cbn.
+ apply IHts; intros; apply hfv; now right.
Qed.
Lemma OuterSkolemization_isFunc :
forall (t : Term) (F : Form) (symbs : sko_record OuterSkolemizationData) (fvs : set_var)
(func_symbols : set_func) (hsko : OuterSkolemizationData t F symbs fvs func_symbols = true),
t = Fun (symbol OuterSkolemizationData hsko) (args OuterSkolemizationData hsko).
Proof using Type.
intros. destruct t; cbn in *; try (inversion hsko; fail).
reflexivity.
Qed.
Lemma OuterSkolemization_function_symbols :
forall {t : Term} {F : Form} {symbs : sko_record OuterSkolemizationData} {fvs : set_var}
{func_symbols : set_func} (hsko : OuterSkolemizationData t F symbs fvs func_symbols = true),
function_symbols (args OuterSkolemizationData hsko) = \{\}.
Proof using Type.
intros; destruct t; try (inversion hsko; fail); cbn in hsko |- *;
unfold OuterSkolemization_is_sko_pred in hsko.
have hsko' := andb_prop _ _ hsko.
destruct hsko' as (_ & hfree); clear hsko.
induction l as [|t ts IHts]; auto; cbn.
cbn in hfree; apply andb_prop in hfree; destruct hfree as [hfreet hfreets].
rewrite set_fold_left empty_unitl IHts; auto.
destruct t; try inversion hfreet; cbn; apply empty_unitl.
Qed.
Lemma isSkolemization_OuterSkolemizationData :
isSkolemization OuterSkolemizationData.
Proof using set_nat.
constructor.
- apply OuterSkolemization_isFunc.
- intros ??????? hin. destruct t; try easy.
have [ _ [ _ [ _ hfree ] ] ] := OuterSkolemization_is_sko_pred_sound _ _ _ _ _ hsko.
now apply hfree.
- intros ?????? hsubset e; cbn in *.
destruct t; try easy; cbn in *.
unfold OuterSkolemization_is_sko_pred. rewrite andb_true_intro; split; auto.
+ rewrite andb_true_intro; split; auto.
* rewrite andb_true_intro; split; auto.
-- rewrite Bool.negb_true_iff mem_spec'; intro.
apply OuterSkolemization_is_sko_pred_sound in e; destruct e as [hin _].
now apply hin, hsubset.
-- apply OuterSkolemization_is_sko_pred_sound in e; destruct e as [ _ [hsub _] ].
rewrite subsetb_spec //.
* apply OuterSkolemization_is_sko_pred_sound in e; destruct e as [ _ [_ [ e _ ] ] ].
rewrite eqbIsEq //.
+ apply andb_prop in e; now destruct e.
- intros ????? hsko ?.
destruct t; try inversion hsko.
destruct (OuterSkolemization_args_vars hsko) as (l0 & el0).
cbn in el0. rewrite el0.
exists (replace_interp_func M F (symbol OuterSkolemizationData hsko) l0); split.
+ intros mu hdelta; apply satisfies_opening_with_sko; auto.
* destruct (OuterSkolemization_is_sko_pred_sound _ _ _ _ _ H3) as (_ & hfvs & e & _).
intros x hin; specialize (hfvs x hin). rewrite -e in hfvs. rewrite el0 in hfvs.
clear hsko e H3 el0; induction l0 as [|v vs IHvs].
-- now apply empty_spec in hfvs.
-- cbn; rewrite union_spec. cbn in hfvs; rewrite union_spec in hfvs.
destruct hfvs.
++ now left.
++ right; now apply IHvs.
* destruct (OuterSkolemization_is_sko_pred_sound _ _ _ _ _ H3) as (hnin & _ & _).
intro hin; now apply hnin, hdelta.
+ intros G mu hG. unfold interpret; rewrite no_skolem_same_interp_form; auto.
destruct (OuterSkolemization_is_sko_pred_sound _ _ _ _ _ H3) as (hnin & _ & _); cbn.
intro hin; now apply hnin, hG.
Qed.
Definition OuterSkolemization : Skolemization_ pred func var.
Proof.
unshelve econstructor.
- exact OuterSkolemizationData.
- exact isSkolemization_OuterSkolemizationData.
Defined.
(func_symbols : set_func) (f : func) (l : list Term) : bool :=
negb (mem f func_symbols) && subsetb (fv F) fvs &&
eqb (fv l) fvs && forallb is_free l.
Lemma OuterSkolemization_is_sko_pred_sound :
forall (fvs : set_var) (func_symbols : set_func) (F : Form) (f : func) (l : list Term),
OuterSkolemization_is_sko_pred F fvs func_symbols f l = true ->
~(set_in f func_symbols) /\ fv F \subseteq fvs /\ fv l = fvs /\
(forall (t : Term), List.In t l -> exists (x : var), t = Free x).
Proof using Type.
intros ????? [ [ [hfresh%Bool.negb_true_iff hsub]%andb_prop e ]%andb_prop hfree ]%andb_prop;
repeat split.
- rewrite -mem_spec' //.
- now rewrite subsetb_spec in hsub.
- rewrite -eqbIsEq //.
- rewrite forallb_forall in hfree; intros ? hin; specialize (hfree t hin).
now apply is_free_sound in hfree.
Qed.
Definition OuterSkolemizationData : SkolemizationData pred func var.
Proof.
unshelve econstructor.
- exact sko_record_set.
(* in outer skolemization, we simply need to keep track of which symbols have been
instantiated *)
- intros t F _ fvs symbs2.
exact (SkoWrapper_is_sko t (OuterSkolemization_is_sko_pred F fvs symbs2)).
- intros t ???? hsko. apply (SkoWrapper_symbol t hsko).
- intros t ???? hsko. apply (SkoWrapper_args t hsko).
Defined.
Lemma OuterSkolemization_args_vars :
forall {func_symbols : set_func} {t : Term} {F : Form} {symbs : sko_record OuterSkolemizationData}
{fvs : set_var} (hsko : OuterSkolemizationData t F symbs fvs func_symbols = true),
exists (l : list var), args OuterSkolemizationData hsko =
map (fun v => Free v) l.
Proof using Type.
intros ??????. set largs := args OuterSkolemizationData hsko.
destruct t; try inversion hsko; cbn in hsko.
have eargs : largs = l by reflexivity. rewrite eargs.
have [ _ [ _ [ _ hargs ] ] ] := OuterSkolemization_is_sko_pred_sound _ _ _ _ _ H3.
clear largs eargs H3 hsko.
induction l as [|t ts IHts].
- now exists [].
- have ht := hargs t ltac:(now left).
destruct ht as (x & e).
have h : forall t, List.In t ts -> exists x : var, t = Free x.
{ intros; apply hargs. now right. }
specialize (IHts h). destruct IHts as (l0 & el0).
exists (x :: l0); cbn. rewrite e el0 //.
Qed.
Lemma OuterSkolemization_isLocallyClosed :
forall (t : Term) (F : Form) (symbs : sko_record OuterSkolemizationData) (fvs : set_var)
(func_symbols : set_func),
OuterSkolemizationData t F symbs fvs func_symbols = true -> isLocallyClosed t.
Proof using Type.
intros ????? hsko; destruct t; cbn in *; try (inversion hsko; fail).
apply OuterSkolemization_is_sko_pred_sound in hsko; destruct hsko as (_ & _ & _ & hfv).
clear func_symbols symbs F; induction l as [|t ts IHts]; unfold isLocallyClosed; cbn;
unfold is_empty; auto.
change (bv t \union bv_list ts = \{\}); apply is_empty_union; split.
+ have h : exists x, t = Free x by apply hfv; now left.
destruct h as (x & e); rewrite e; now cbn.
+ apply IHts; intros; apply hfv; now right.
Qed.
Lemma OuterSkolemization_isFunc :
forall (t : Term) (F : Form) (symbs : sko_record OuterSkolemizationData) (fvs : set_var)
(func_symbols : set_func) (hsko : OuterSkolemizationData t F symbs fvs func_symbols = true),
t = Fun (symbol OuterSkolemizationData hsko) (args OuterSkolemizationData hsko).
Proof using Type.
intros. destruct t; cbn in *; try (inversion hsko; fail).
reflexivity.
Qed.
Lemma OuterSkolemization_function_symbols :
forall {t : Term} {F : Form} {symbs : sko_record OuterSkolemizationData} {fvs : set_var}
{func_symbols : set_func} (hsko : OuterSkolemizationData t F symbs fvs func_symbols = true),
function_symbols (args OuterSkolemizationData hsko) = \{\}.
Proof using Type.
intros; destruct t; try (inversion hsko; fail); cbn in hsko |- *;
unfold OuterSkolemization_is_sko_pred in hsko.
have hsko' := andb_prop _ _ hsko.
destruct hsko' as (_ & hfree); clear hsko.
induction l as [|t ts IHts]; auto; cbn.
cbn in hfree; apply andb_prop in hfree; destruct hfree as [hfreet hfreets].
rewrite set_fold_left empty_unitl IHts; auto.
destruct t; try inversion hfreet; cbn; apply empty_unitl.
Qed.
Lemma isSkolemization_OuterSkolemizationData :
isSkolemization OuterSkolemizationData.
Proof using set_nat.
constructor.
- apply OuterSkolemization_isFunc.
- intros ??????? hin. destruct t; try easy.
have [ _ [ _ [ _ hfree ] ] ] := OuterSkolemization_is_sko_pred_sound _ _ _ _ _ hsko.
now apply hfree.
- intros ?????? hsubset e; cbn in *.
destruct t; try easy; cbn in *.
unfold OuterSkolemization_is_sko_pred. rewrite andb_true_intro; split; auto.
+ rewrite andb_true_intro; split; auto.
* rewrite andb_true_intro; split; auto.
-- rewrite Bool.negb_true_iff mem_spec'; intro.
apply OuterSkolemization_is_sko_pred_sound in e; destruct e as [hin _].
now apply hin, hsubset.
-- apply OuterSkolemization_is_sko_pred_sound in e; destruct e as [ _ [hsub _] ].
rewrite subsetb_spec //.
* apply OuterSkolemization_is_sko_pred_sound in e; destruct e as [ _ [_ [ e _ ] ] ].
rewrite eqbIsEq //.
+ apply andb_prop in e; now destruct e.
- intros ????? hsko ?.
destruct t; try inversion hsko.
destruct (OuterSkolemization_args_vars hsko) as (l0 & el0).
cbn in el0. rewrite el0.
exists (replace_interp_func M F (symbol OuterSkolemizationData hsko) l0); split.
+ intros mu hdelta; apply satisfies_opening_with_sko; auto.
* destruct (OuterSkolemization_is_sko_pred_sound _ _ _ _ _ H3) as (_ & hfvs & e & _).
intros x hin; specialize (hfvs x hin). rewrite -e in hfvs. rewrite el0 in hfvs.
clear hsko e H3 el0; induction l0 as [|v vs IHvs].
-- now apply empty_spec in hfvs.
-- cbn; rewrite union_spec. cbn in hfvs; rewrite union_spec in hfvs.
destruct hfvs.
++ now left.
++ right; now apply IHvs.
* destruct (OuterSkolemization_is_sko_pred_sound _ _ _ _ _ H3) as (hnin & _ & _).
intro hin; now apply hnin, hdelta.
+ intros G mu hG. unfold interpret; rewrite no_skolem_same_interp_form; auto.
destruct (OuterSkolemization_is_sko_pred_sound _ _ _ _ _ H3) as (hnin & _ & _); cbn.
intro hin; now apply hnin, hG.
Qed.
Definition OuterSkolemization : Skolemization_ pred func var.
Proof.
unshelve econstructor.
- exact OuterSkolemizationData.
- exact isSkolemization_OuterSkolemizationData.
Defined.
In inner skolemization, we want to check that:
As the fact that it's a functorial term is already given by SkoWrapper_is_sko,
we focus on defining the other aspects here.
- t is a functorial term f (t1, ..., tn),
- such that f does not already appear in Gamma,
- and t1, ..., tn are actually all the free variables of the formula.
Definition InnerSkolemization_is_sko_pred (F : Form) (func_symbols : set_func) (f : func)
(l : list Term) : bool :=
negb (mem f func_symbols) &&
eqb (fv l) (fv F) && forallb is_free l.
Lemma InnerSkolemization_is_sko_pred_sound :
forall (F : Form) (func_symbols : set_func) (f : func) (l : list Term),
InnerSkolemization_is_sko_pred F func_symbols f l = true ->
~(set_in f func_symbols) /\
fv l = fv F /\
(forall (t : Term), List.In t l -> exists (x : var), t = Free x).
Proof using Type.
intros ???? [ [ hfresh%Bool.negb_true_iff e ]%andb_prop hfree ]%andb_prop;
repeat split.
- rewrite -mem_spec' //.
- rewrite -eqbIsEq //.
- rewrite forallb_forall in hfree; intros ? hin; specialize (hfree t hin).
now apply is_free_sound in hfree.
Qed.
Definition InnerSkolemizationData : SkolemizationData pred func var.
Proof.
unshelve econstructor.
- exact sko_record_set.
- intros t F _ _ func_symbols.
exact (SkoWrapper_is_sko t (InnerSkolemization_is_sko_pred F func_symbols)).
- intros t ???? hsko. apply (SkoWrapper_symbol t hsko).
- intros t ???? hsko. apply (SkoWrapper_args t hsko).
Defined.
Lemma InnerSkolemization_args_vars :
forall {func_symbols : set_func} {t : Term} {F : Form}
{symbs : sko_record InnerSkolemizationData} {fvs : set_var}
(hsko : InnerSkolemizationData t F symbs fvs func_symbols = true),
exists (l : list var), args InnerSkolemizationData hsko =
map (fun v => Free v) l.
Proof using Type.
intros ??????. set largs := args InnerSkolemizationData hsko.
destruct t; try inversion hsko; cbn in hsko.
have eargs : largs = l by reflexivity. rewrite eargs.
have [ _ [ _ hargs ] ] := InnerSkolemization_is_sko_pred_sound _ _ _ _ H3.
clear largs eargs H3 hsko.
induction l as [|t ts IHts].
- now exists [].
- have ht := hargs t ltac:(now left).
destruct ht as (x & e).
have h : forall t, List.In t ts -> exists x : var, t = Free x.
{ intros; apply hargs. now right. }
specialize (IHts h). destruct IHts as (l0 & el0).
exists (x :: l0); cbn. rewrite e el0 //.
Qed.
Lemma InnerSkolemization_isLocallyClosed :
forall (t : Term) (F : Form) (symbs : sko_record InnerSkolemizationData) (fvs : set_var)
(func_symbols : set_func),
InnerSkolemizationData t F symbs fvs func_symbols = true -> isLocallyClosed t.
Proof using Type.
intros ????? hsko; destruct t; cbn in *; try (inversion hsko; fail).
apply InnerSkolemization_is_sko_pred_sound in hsko; destruct hsko as (_ & _ & hfv).
clear func_symbols symbs F; induction l as [|t ts IHts]; unfold isLocallyClosed; cbn;
unfold is_empty; auto.
change (bv t \union bv_list ts = \{\}); apply is_empty_union; split.
+ have h : exists x, t = Free x by apply hfv; now left.
destruct h as (x & e); rewrite e; now cbn.
+ apply IHts; intros; apply hfv; now right.
Qed.
Lemma InnerSkolemization_isFunc :
forall (t : Term) (F : Form) (symbs : sko_record InnerSkolemizationData) (fvs : set_var)
(func_symbols : set_func) (hsko : InnerSkolemizationData t F symbs fvs func_symbols = true),
t = Fun (symbol InnerSkolemizationData hsko) (args InnerSkolemizationData hsko).
Proof using Type.
intros. destruct t; cbn in *; try (inversion hsko; fail).
reflexivity.
Qed.
Lemma InnerSkolemization_function_symbols :
forall {t : Term} {F : Form} {symbs : sko_record InnerSkolemizationData} {fvs : set_var}
{func_symbols : set_func} (hsko : InnerSkolemizationData t F symbs fvs func_symbols = true),
function_symbols (args InnerSkolemizationData hsko) = \{\}.
Proof using Type.
intros; destruct t; try (inversion hsko; fail); cbn in hsko |- *;
unfold InnerSkolemization_is_sko_pred in hsko.
have hsko' := andb_prop _ _ hsko.
destruct hsko' as (_ & hfree); clear hsko.
induction l as [|t ts IHts]; auto; cbn.
cbn in hfree; apply andb_prop in hfree; destruct hfree as [hfreet hfreets].
rewrite set_fold_left empty_unitl IHts; auto.
destruct t; try inversion hfreet; cbn; apply empty_unitl.
Qed.
Lemma isSkolemization_InnerSkolemizationData :
isSkolemization InnerSkolemizationData.
Proof using set_nat.
constructor.
- apply InnerSkolemization_isFunc.
- intros ??????? hin. destruct t; try easy.
have [ _ [ _ hfree ] ] := InnerSkolemization_is_sko_pred_sound _ _ _ _ hsko.
now apply hfree.
- intros ?????? hsubset e; cbn in *.
destruct t; try easy; cbn in *.
unfold InnerSkolemization_is_sko_pred. rewrite andb_true_intro; split; auto.
+ rewrite andb_true_intro; split; auto.
* rewrite Bool.negb_true_iff mem_spec'; intro.
apply InnerSkolemization_is_sko_pred_sound in e; destruct e as [hin _].
now apply hin, hsubset.
* apply InnerSkolemization_is_sko_pred_sound in e; destruct e as [ _ [e _] ].
rewrite eqbIsEq //.
+ apply andb_prop in e; now destruct e. - intros ????? hsko ?.
destruct t; try inversion hsko.
destruct (InnerSkolemization_args_vars hsko) as (l0 & el0).
cbn in el0. rewrite el0.
exists (replace_interp_func M F (symbol InnerSkolemizationData hsko) l0); split.
+ intros mu hdelta; apply satisfies_opening_with_sko; auto.
* destruct (InnerSkolemization_is_sko_pred_sound _ _ _ _ H3) as (_ & e & _).
rewrite el0 in e; cbn in e. rewrite -e.
clear. induction l0 as [|v vs IHvs].
-- now intros x hin%empty_spec.
-- cbn; intros x hin; rewrite !union_spec in hin |- *.
destruct hin.
++ now left.
++ right; now apply IHvs.
* destruct (InnerSkolemization_is_sko_pred_sound _ _ _ _ H3) as (hnin & _ & _).
intro hin; now apply hnin, hdelta.
+ intros G mu hG. unfold interpret; rewrite no_skolem_same_interp_form; auto.
destruct (InnerSkolemization_is_sko_pred_sound _ _ _ _ H3) as (hnin & _ & _); cbn.
intro hin. now apply hnin, hG.
Qed.
Definition InnerSkolemization : Skolemization_ pred func var.
Proof.
unshelve econstructor.
- exact InnerSkolemizationData.
- exact isSkolemization_InnerSkolemizationData.
Defined.
End SkolemizationInstances.
(l : list Term) : bool :=
negb (mem f func_symbols) &&
eqb (fv l) (fv F) && forallb is_free l.
Lemma InnerSkolemization_is_sko_pred_sound :
forall (F : Form) (func_symbols : set_func) (f : func) (l : list Term),
InnerSkolemization_is_sko_pred F func_symbols f l = true ->
~(set_in f func_symbols) /\
fv l = fv F /\
(forall (t : Term), List.In t l -> exists (x : var), t = Free x).
Proof using Type.
intros ???? [ [ hfresh%Bool.negb_true_iff e ]%andb_prop hfree ]%andb_prop;
repeat split.
- rewrite -mem_spec' //.
- rewrite -eqbIsEq //.
- rewrite forallb_forall in hfree; intros ? hin; specialize (hfree t hin).
now apply is_free_sound in hfree.
Qed.
Definition InnerSkolemizationData : SkolemizationData pred func var.
Proof.
unshelve econstructor.
- exact sko_record_set.
- intros t F _ _ func_symbols.
exact (SkoWrapper_is_sko t (InnerSkolemization_is_sko_pred F func_symbols)).
- intros t ???? hsko. apply (SkoWrapper_symbol t hsko).
- intros t ???? hsko. apply (SkoWrapper_args t hsko).
Defined.
Lemma InnerSkolemization_args_vars :
forall {func_symbols : set_func} {t : Term} {F : Form}
{symbs : sko_record InnerSkolemizationData} {fvs : set_var}
(hsko : InnerSkolemizationData t F symbs fvs func_symbols = true),
exists (l : list var), args InnerSkolemizationData hsko =
map (fun v => Free v) l.
Proof using Type.
intros ??????. set largs := args InnerSkolemizationData hsko.
destruct t; try inversion hsko; cbn in hsko.
have eargs : largs = l by reflexivity. rewrite eargs.
have [ _ [ _ hargs ] ] := InnerSkolemization_is_sko_pred_sound _ _ _ _ H3.
clear largs eargs H3 hsko.
induction l as [|t ts IHts].
- now exists [].
- have ht := hargs t ltac:(now left).
destruct ht as (x & e).
have h : forall t, List.In t ts -> exists x : var, t = Free x.
{ intros; apply hargs. now right. }
specialize (IHts h). destruct IHts as (l0 & el0).
exists (x :: l0); cbn. rewrite e el0 //.
Qed.
Lemma InnerSkolemization_isLocallyClosed :
forall (t : Term) (F : Form) (symbs : sko_record InnerSkolemizationData) (fvs : set_var)
(func_symbols : set_func),
InnerSkolemizationData t F symbs fvs func_symbols = true -> isLocallyClosed t.
Proof using Type.
intros ????? hsko; destruct t; cbn in *; try (inversion hsko; fail).
apply InnerSkolemization_is_sko_pred_sound in hsko; destruct hsko as (_ & _ & hfv).
clear func_symbols symbs F; induction l as [|t ts IHts]; unfold isLocallyClosed; cbn;
unfold is_empty; auto.
change (bv t \union bv_list ts = \{\}); apply is_empty_union; split.
+ have h : exists x, t = Free x by apply hfv; now left.
destruct h as (x & e); rewrite e; now cbn.
+ apply IHts; intros; apply hfv; now right.
Qed.
Lemma InnerSkolemization_isFunc :
forall (t : Term) (F : Form) (symbs : sko_record InnerSkolemizationData) (fvs : set_var)
(func_symbols : set_func) (hsko : InnerSkolemizationData t F symbs fvs func_symbols = true),
t = Fun (symbol InnerSkolemizationData hsko) (args InnerSkolemizationData hsko).
Proof using Type.
intros. destruct t; cbn in *; try (inversion hsko; fail).
reflexivity.
Qed.
Lemma InnerSkolemization_function_symbols :
forall {t : Term} {F : Form} {symbs : sko_record InnerSkolemizationData} {fvs : set_var}
{func_symbols : set_func} (hsko : InnerSkolemizationData t F symbs fvs func_symbols = true),
function_symbols (args InnerSkolemizationData hsko) = \{\}.
Proof using Type.
intros; destruct t; try (inversion hsko; fail); cbn in hsko |- *;
unfold InnerSkolemization_is_sko_pred in hsko.
have hsko' := andb_prop _ _ hsko.
destruct hsko' as (_ & hfree); clear hsko.
induction l as [|t ts IHts]; auto; cbn.
cbn in hfree; apply andb_prop in hfree; destruct hfree as [hfreet hfreets].
rewrite set_fold_left empty_unitl IHts; auto.
destruct t; try inversion hfreet; cbn; apply empty_unitl.
Qed.
Lemma isSkolemization_InnerSkolemizationData :
isSkolemization InnerSkolemizationData.
Proof using set_nat.
constructor.
- apply InnerSkolemization_isFunc.
- intros ??????? hin. destruct t; try easy.
have [ _ [ _ hfree ] ] := InnerSkolemization_is_sko_pred_sound _ _ _ _ hsko.
now apply hfree.
- intros ?????? hsubset e; cbn in *.
destruct t; try easy; cbn in *.
unfold InnerSkolemization_is_sko_pred. rewrite andb_true_intro; split; auto.
+ rewrite andb_true_intro; split; auto.
* rewrite Bool.negb_true_iff mem_spec'; intro.
apply InnerSkolemization_is_sko_pred_sound in e; destruct e as [hin _].
now apply hin, hsubset.
* apply InnerSkolemization_is_sko_pred_sound in e; destruct e as [ _ [e _] ].
rewrite eqbIsEq //.
+ apply andb_prop in e; now destruct e. - intros ????? hsko ?.
destruct t; try inversion hsko.
destruct (InnerSkolemization_args_vars hsko) as (l0 & el0).
cbn in el0. rewrite el0.
exists (replace_interp_func M F (symbol InnerSkolemizationData hsko) l0); split.
+ intros mu hdelta; apply satisfies_opening_with_sko; auto.
* destruct (InnerSkolemization_is_sko_pred_sound _ _ _ _ H3) as (_ & e & _).
rewrite el0 in e; cbn in e. rewrite -e.
clear. induction l0 as [|v vs IHvs].
-- now intros x hin%empty_spec.
-- cbn; intros x hin; rewrite !union_spec in hin |- *.
destruct hin.
++ now left.
++ right; now apply IHvs.
* destruct (InnerSkolemization_is_sko_pred_sound _ _ _ _ H3) as (hnin & _ & _).
intro hin; now apply hnin, hdelta.
+ intros G mu hG. unfold interpret; rewrite no_skolem_same_interp_form; auto.
destruct (InnerSkolemization_is_sko_pred_sound _ _ _ _ H3) as (hnin & _ & _); cbn.
intro hin. now apply hnin, hG.
Qed.
Definition InnerSkolemization : Skolemization_ pred func var.
Proof.
unshelve econstructor.
- exact InnerSkolemizationData.
- exact isSkolemization_InnerSkolemizationData.
Defined.
End SkolemizationInstances.
Instances of Skolemization with the concrete syntax can be found in SkolemizationInstances.v.