Commit e2852c81 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Theoreme de Skolem : l'extension de Skolem pour un theorem \forall\exists est conservative

parent fedfec2c
......@@ -8,7 +8,7 @@
# #
###############################################################################
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Restrict.v Meta.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v PreModels.v Models.v Peano.v ZF.v
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Restrict.v Meta.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v PreModels.v Models.v Skolem.v Peano.v ZF.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
......
......@@ -13,7 +13,15 @@ Local Open Scope eqb_scope.
Implicit Type t u : term.
Implicit Type f : formula.
(** [lift] does nothing on a [BClosed] term *)
(** Properties of [lift] *)
Lemma level_lift t : level (lift t) <= S (level t).
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with arith.
rewrite map_map.
apply list_max_map_le. intros a Ha. transitivity (S (level a)); auto.
rewrite <- Nat.succ_le_mono. now apply list_max_map_in.
Qed.
Lemma lift_nop t : BClosed t -> lift t = t.
Proof.
......@@ -23,33 +31,25 @@ Proof.
- rewrite list_max_map_0. intros H. f_equal. apply map_id_iff; auto.
Qed.
(** [check] and [lift_above] *)
Lemma check_lift_above sign t k :
check sign (lift_above k t) = check sign t.
Lemma check_lift sign t :
check sign (lift t) = check sign t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
+ destruct (k <=? n); auto.
+ destruct funsymbs; auto.
rewrite map_length. case eqb; auto.
apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
split; intros H x Hx. rewrite<- IH; auto. rewrite IH; auto.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
destruct funsymbs; auto.
rewrite map_length. case eqb; auto.
apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
split; intros H x Hx. rewrite <- IH; auto. rewrite IH; auto.
Qed.
Lemma check_lift_form_above sign f k :
check sign (lift_form_above k f) = check sign f.
Lemma lift_fvars t : fvars (lift t) = fvars t.
Proof.
revert k. induction f; cbn; auto.
+ destruct (predsymbs sign p); auto.
intro. rewrite map_length. case eqb; auto.
apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
split; intros.
- destruct H with (x := x); auto. rewrite check_lift_above. reflexivity.
- destruct H with (x := x); auto. rewrite check_lift_above. reflexivity.
+ intro. rewrite IHf1. rewrite IHf2. reflexivity.
induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
induction l; simpl; auto.
rewrite IH, IHl; simpl; auto.
intros x Hx. apply IH. simpl; auto.
Qed.
(** [level] and [lift_above] *)
(** Properties of [lift_above] *)
Lemma level_lift_above t k :
level (lift_above k t) <= S (level t).
......@@ -61,8 +61,6 @@ Proof.
rewrite<- Nat.succ_le_mono. now apply list_max_map_in.
Qed.
Ltac specialise t := specialize t.
Lemma level_lift_form_above f k :
level (lift_form_above k f) <= S (level f).
Proof.
......@@ -75,14 +73,36 @@ Proof.
- apply-> Nat.succ_le_mono.
apply list_max_map_in.
assumption.
+ specialise (IHf1 k).
specialise (IHf2 k).
+ specialize (IHf1 k).
specialize (IHf2 k).
omega with *.
+ specialise (IHf (S k)).
+ specialize (IHf (S k)).
omega.
Qed.
(** [fvars] and [lift_above] *)
Lemma check_lift_above sign t k :
check sign (lift_above k t) = check sign t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
+ destruct (k <=? n); auto.
+ destruct funsymbs; auto.
rewrite map_length. case eqb; auto.
apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
split; intros H x Hx. rewrite<- IH; auto. rewrite IH; auto.
Qed.
Lemma check_lift_form_above sign f k :
check sign (lift_form_above k f) = check sign f.
Proof.
revert k. induction f; cbn; auto.
+ destruct (predsymbs sign p); auto.
intro. rewrite map_length. case eqb; auto.
apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
split; intros.
- destruct H with (x := x); auto. rewrite check_lift_above. reflexivity.
- destruct H with (x := x); auto. rewrite check_lift_above. reflexivity.
+ intro. rewrite IHf1. rewrite IHf2. reflexivity.
Qed.
Lemma fvars_lift_above t k :
fvars (lift_above k t) = fvars t.
......@@ -105,16 +125,6 @@ Qed.
(** [bsubst] and [check] *)
Lemma check_lift sign t :
check sign (lift t) = check sign t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
destruct funsymbs; auto.
rewrite map_length. case eqb; auto.
apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
split; intros H x Hx. rewrite <- IH; auto. rewrite IH; auto.
Qed.
Lemma check_bsubst_term sign n (u t:term) :
check sign u = true -> check sign t = true ->
check sign (bsubst n u t) = true.
......@@ -144,12 +154,26 @@ Qed.
(** [bsubst] and [level] *)
Lemma level_lift t : level (lift t) <= S (level t).
Lemma level_bsubst_term_max n (u t:term) :
level (bsubst n u t) <= Nat.max (level u) (level t).
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with arith.
rewrite map_map.
apply list_max_map_le. intros a Ha. transitivity (S (level a)); auto.
rewrite <- Nat.succ_le_mono. now apply list_max_map_in.
revert t. fix IH 1; destruct t; cbn -[Nat.max].
- auto with arith.
- case eqbspec; cbn -[Nat.max]; omega with *.
- revert l. fix IHl 1; destruct l; cbn -[Nat.max].
+ auto with arith.
+ specialize (IH t). specialize (IHl l). omega with *.
Qed.
Lemma level_bsubst_max n u (f:formula) :
level (bsubst n u f) <= Nat.max (level u) (level f).
Proof.
revert n u.
induction f; intros; cbn -[Nat.max]; auto with arith.
- apply (level_bsubst_term_max n u (Fun "" l)).
- specialize (IHf1 n u). specialize (IHf2 n u). omega with *.
- assert (H := level_lift u).
specialize (IHf (S n) (lift u)). omega with *.
Qed.
Lemma level_bsubst_term n (u t:term) :
......@@ -196,14 +220,6 @@ Qed.
(** [bsubst] and [fvars] : over-approximations *)
Lemma lift_fvars t : fvars (lift t) = fvars t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
induction l; simpl; auto.
rewrite IH, IHl; simpl; auto.
intros x Hx. apply IH. simpl; auto.
Qed.
Lemma bsubst_term_fvars n (u t:term) :
Names.Subset (fvars (bsubst n u t)) (Names.union (fvars u) (fvars t)).
Proof.
......
......@@ -554,16 +554,7 @@ Proof.
apply R_Fa_e.
apply R_Not_e with A. apply R'_Ax.
eapply Pr_weakening; eauto. constructor. intros a; simpl; auto.
- intros (_ & axsAB & FAB & PRAB) (_ & axsA & FA & PRA).
split. now rewrite Op_wf in WF.
exists (axsAB++axsA). split.
rewrite Forall_forall in *; intros x; rewrite !in_app_iff;
intros [|]; auto.
apply R_Imp_e with A.
+ clear PRA; eapply Pr_weakening; eauto. constructor.
intros a. simpl. rewrite !in_app_iff; auto.
+ clear PRAB; eapply Pr_weakening; eauto. constructor.
intros a. simpl. rewrite !in_app_iff; auto.
- apply ModusPonens.
Qed.
Lemma pr_notex_allnot logic c A :
......
......@@ -439,9 +439,9 @@ Proof.
Qed.
Lemma nForall_fclosed n A :
FClosed A -> FClosed (nForall n A).
FClosed A <-> FClosed (nForall n A).
Proof.
induction n; simpl; auto.
induction n; simpl; easy.
Qed.
Lemma nForall_level n A :
......
(** * First-order theories *)
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import ChoiceFacts.
Require Vector.
Require Import Defs NameProofs Mix Meta Theories PreModels Models.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope eqb_scope.
Notation K := Classic.
Implicit Types th : theory.
(** [downvars n = [#n ; ... ; #1] ]. *)
Fixpoint downvars n :=
match n with
| O => nil
| S n' => BVar n :: downvars n'
end.
Lemma seq_S a n : seq a (S n) = seq a n ++ [n+a].
Proof.
revert a; induction n; cbn; try easy.
intros. f_equal. rewrite <- Nat.add_succ_r.
now rewrite <- IHn.
Qed.
Lemma downvars_alt n : downvars n = rev (map BVar (seq 1 n)).
Proof.
induction n.
- cbn; auto.
- rewrite seq_S. cbn. rewrite map_app, rev_app_distr. cbn.
rewrite Nat.add_1_r. now f_equal.
Qed.
Lemma level_downvars n : n<>0 -> level (downvars n) = S n.
Proof.
induction n; try easy.
destruct n. easy.
intros. set (m := S n) in *.
assert (IH : level (downvars m) = S m) by now apply IHn.
clearbody m. clear IHn.
cbn -[Nat.max]. change (list_max _) with (level (downvars m)).
rewrite IH. omega with *.
Qed.
Lemma level_downvars_le n : level (downvars n) <= S n.
Proof.
destruct n. auto. rewrite level_downvars; auto.
Qed.
Lemma interp_downvars sign M (mo:PreModel M sign) genv n l m :
length l = n ->
map (interp_term mo genv (m :: l)) (downvars n) = rev l.
Proof.
intros E.
rewrite downvars_alt, map_rev. f_equal.
rewrite <- seq_shift, !map_map.
cbn.
revert l E. induction n; destruct l; cbn; intros; try easy.
f_equal. rewrite <- seq_shift, map_map. apply IHn. now injection E.
Qed.
(** N-ary curry / uncurry conversions :
isomorphism between [arity_fun] and functions expecting a [Vector.t]
as first argument. *)
Section Curry.
Context {A B : Type}.
Import Vector.VectorNotations.
Local Notation "A ^ n" := (Vector.t A n) : types_scope.
Local Open Scope types_scope.
Local Open Scope vector_scope.
Fixpoint uncurry {n} : arity_fun A n B -> A^n -> B :=
match n with
| 0 => fun b _ => b
| S n => fun f v => uncurry (f (Vector.hd v)) (Vector.tl v)
end.
Fixpoint curry {n} : (A^n -> B) -> arity_fun A n B :=
match n with
| 0 => fun f => f (Vector.nil _)
| S n => fun f a => curry (fun v => f (a::v))
end.
Lemma uncurry_curry n (phi : A^n -> B) v :
uncurry (curry phi) v = phi v.
Proof.
induction v; cbn; auto. now rewrite IHv.
Qed.
Lemma to_vect n (l:list A) :
length l = n -> exists v : Vector.t A n, Vector.to_list v = l.
Proof.
revert n; induction l as [|a l IH]; simpl.
- intros n <-. now exists [].
- destruct n as [|n]; intros [= E].
destruct (IH n E) as (v & Hv). exists (a::v). cbn; f_equal; auto.
Qed.
End Curry.
(** Skolem extension : from a theorem [..∀∃A],
adding a new symbol [f] giving existential witnesses
and the new axiom [xi A(xi,f(xi))].
*)
Definition Skolem_sign sign f n :=
modify_funsymbs sign
(fun funs s => if s =? f then Some n else funs s).
Lemma Skolem_signext sign f n :
sign.(funsymbs) f = None ->
SignExtend sign (Skolem_sign sign f n).
Proof.
intros Hc.
split; unfold optfun_finer, opt_finer; cbn; auto.
intros a. case eqbspec; intros; subst; auto.
Qed.
(** The Skolem axiom for formula A, new symbol f of arity n.
The n+1 foralls is a hack, the last one is just there for
de Bruijn indices to be correctly aligned. *)
Definition Skolem_axiom A f n :=
nForall (S n) (bsubst 0 (Fun f (downvars n)) A).
Lemma Skolem_axiom_wf sign f n A :
funsymbs sign f = Some n ->
Wf sign (nForall n ( A)) ->
Wf sign (Skolem_axiom A f n).
Proof.
unfold Skolem_axiom.
intros Hf (CA & LA & FA). repeat split.
- rewrite nForall_check, check_bsubst in *; auto.
cbn. rewrite Hf.
clear. induction n; simpl; auto.
- unfold BClosed in *. rewrite nForall_level in *.
cbn in LA.
apply Nat.sub_0_le. etransitivity; [apply level_bsubst_max|].
apply Nat.max_lub; try omega with *.
apply level_downvars_le.
- rewrite <- nForall_fclosed in *.
rewrite <- form_fclosed_spec in *.
cbn in FA. rewrite fclosed_bsubst; auto.
clear. induction n; simpl; auto.
Qed.
Definition SkolemAx Ax (A:formula) f n :=
fun B => Ax B \/ B = Skolem_axiom A f n.
Lemma SkolemAxWf th A f n :
th.(funsymbs) f = None ->
IsTheorem K th (nForall n (A)) ->
forall B, SkolemAx th.(IsAxiom) A f n B -> Wf (Skolem_sign th f n) B.
Proof.
intros Hc (CL & _) B [HB| -> ].
- eauto using signext_wf, Skolem_signext, WfAxiom.
- apply Skolem_axiom_wf.
+ simpl. now rewrite eqb_refl.
+ eauto using signext_wf, Skolem_signext.
Qed.
Definition Skolem_ext th A f n
(E:th.(funsymbs) f = None)
(Thm:IsTheorem K th (nForall n (A))) :=
{| sign := Skolem_sign th f n;
IsAxiom := SkolemAx th.(IsAxiom) A f n;
WfAxiom := SkolemAxWf th A f n E Thm |}.
Section SkolemTheorem.
Variable EM : forall A:Prop, A\/~A.
Variable Choice : forall A B, FunctionalChoice_on A B.
Variable th : theory.
Variable NC : NewCsts th.
Definition Skolem_premodel_ext sign M (mo:PreModel M sign)
f n (phi : arity_fun M n M) : PreModel M (Skolem_sign sign f n).
Proof.
set (sign' := Skolem_sign _ _ _).
set (funs' := fun s => if s =? f then Some (existT _ n phi) else funs mo s).
eapply (Build_PreModel sign' (someone mo) funs' (preds mo)); intros s.
- unfold funs'. cbn. case eqbspec; intros; auto using funsOk.
- cbn. apply predsOk.
Defined.
Lemma interp_form_premodel_ext sign sign' M
(mo:PreModel M sign) (mo':PreModel M sign') :
(someone mo = someone mo') ->
(forall f, funs mo f = None \/ funs mo f = funs mo' f) ->
(forall p, preds mo p = preds mo' p) ->
(forall A, check sign A = true ->
forall genv lenv,
interp_form mo genv lenv A <-> interp_form mo' genv lenv A).
Proof.
intros SO FU PR.
assert (Ht : forall (t:term), check sign t = true ->
forall genv lenv, interp_term mo genv lenv t =
interp_term mo' genv lenv t).
{ induction t as [ | | f l IH] using term_ind'; cbn; trivial.
- unfold BogusPoint. now rewrite <- SO.
- destruct (funsymbs sign f) as [ar|] eqn:E; try easy.
rewrite <- andb_lazy_alt, andb_true_iff. intros (_ & F) genv lenv.
destruct (FU f) as [Hf|Hf].
+ exfalso. now rewrite (funsOk mo f), Hf in E.
+ rewrite <- Hf. destruct (funs mo f) as [(p,q)|]; auto.
unfold BogusPoint. rewrite <- SO. f_equal.
apply map_ext_in. intros a Ha.
apply IH; auto. rewrite forallb_forall in F; auto. }
induction A; cbn.
- intuition.
- intuition.
- destruct (predsymbs sign p) as [ar|] eqn:E; try easy.
rewrite <- andb_lazy_alt, andb_true_iff. intros (_ & F) genv lenv.
rewrite <- PR. destruct (preds mo p) as [(u,v)|]; try easy.
f_equiv. apply map_ext_in. intros a Ha. apply Ht.
rewrite forallb_forall in F; auto.
- intros WA genv lenv. now rewrite IHA.
- rewrite <- andb_lazy_alt, andb_true_iff.
intros (WA1,WA2) genv lenv.
specialize (IHA1 WA1 genv lenv).
specialize (IHA2 WA2 genv lenv).
destruct o; cbn; now rewrite IHA1, IHA2.
- intros WA genv lenv.
destruct q; setoid_rewrite IHA; firstorder.
Qed.
Lemma interp_form_skolem_premodel_ext sign M f n (F:arity_fun M n M)
(mo:PreModel M sign) (mo':PreModel M (Skolem_sign sign f n))
(E':mo'=Skolem_premodel_ext sign M mo f n F)
(E:sign.(funsymbs) f = None) :
forall A, check sign A = true ->
forall genv lenv,
interp_form mo genv lenv A <-> interp_form mo' genv lenv A.
Proof.
apply interp_form_premodel_ext; rewrite E'; try easy.
intros f0. unfold Skolem_premodel_ext. cbn.
case eqbspec; auto.
intros ->. left. rewrite (funsOk mo f) in E.
now destruct (funs mo f) as [(p,q)|].
Qed.
Definition interp_phi {n th M} (mo:Model M th)(phi : Vector.t M n -> M) A :=
forall genv v, interp_form mo genv (phi v :: rev (Vector.to_list v)) A.
Definition Skolem_model_AxOk A f n
(E:th.(funsymbs) f = None)
(Thm:IsTheorem K th (nForall n (A)))
M (mo:Model M th)(phi : Vector.t M n -> M)(Hphi : interp_phi mo phi A) :
forall A0 : formula,
IsAxiom (Skolem_ext th A f n E Thm) A0 ->
forall genv : variable -> M,
interp_form (Skolem_premodel_ext th M mo f n (curry phi)) genv [] A0.
Proof.
set (th' := Skolem_ext _ _ _ _ _ _) in *.
set (Phi := curry phi).
set (mo' := Skolem_premodel_ext _ _ _ _ _ _).
intros A0 [ | -> ] genv.
- unfold th'. simpl.
rewrite <- (interp_form_skolem_premodel_ext th M f n Phi mo); auto.
+ now apply AxOk.
+ now apply WfAxiom.
- unfold Skolem_axiom.
rewrite interp_nforall. intros. rewrite app_nil_r.
destruct stk as [|m l]; try easy.
injection H as H.
rewrite <- rev_length in H.
destruct (to_vect _ _ H) as (v & Hv).
rewrite interp_form_bsubst_gen with (lenv' := phi v :: l); auto.
+ unfold th'. simpl.
rewrite <- (interp_form_skolem_premodel_ext th M f n Phi mo); auto.
* rewrite <- (rev_involutive l), <- Hv. apply Hphi.
* clear -Thm. destruct Thm as ((CA & _ & _),_).
rewrite nForall_check in CA. apply CA.
+ simpl nth_error. f_equal.
cbn. rewrite eqb_refl.
rewrite interp_downvars, <- Hv by (now rewrite rev_length in H).
symmetry. clear -v. unfold Phi.
rewrite <- (uncurry_curry _ phi v). induction v; cbn; auto.
+ destruct k; try easy.
Qed.
Definition Skolem_model_ext A f n
(E:th.(funsymbs) f = None)
(Thm:IsTheorem K th (nForall n (A)))
M (mo:Model M th)(phi : Vector.t M n -> M)(Hphi : interp_phi mo phi A) :
Model M (Skolem_ext th A f n E Thm).
Proof.
set (th' := Skolem_ext _ _ _ _ _ _).
apply (Build_Model _ th' (Skolem_premodel_ext th M mo f n (curry phi))).
apply Skolem_model_AxOk; auto.
Defined.
Lemma Skolem_consext A f n
(E:th.(funsymbs) f = None)
(Thm:IsTheorem K th (nForall n (A))) :
ConservativeExt K th (Skolem_ext th A f n E Thm).
Proof.
apply consext_alt.
split.
- rewrite extend_alt. split.
+ now apply Skolem_signext.
+ intros B HB. split.
* apply signext_wf with th.
now apply Skolem_signext.
now apply WfAxiom.
* exists [B]. split. constructor; auto. simpl. red. now left.
apply R'_Ax.
- intros T HT CT.
apply completeness_theorem; auto.
+ split; auto. apply HT.
+ intros M mo genv.
set (th' := Skolem_ext _ _ _ _ _ _) in *.
assert (interp_form mo genv [] (nForall n ( A))).
{ eapply validity_theorem; eauto. red; auto. }
rewrite interp_nforall in H.
assert (C : forall (v : Vector.t M n), exists m,
interp_form mo genv (m::rev (Vector.to_list v)) A).
{ intros v.
specialize (H (rev (Vector.to_list v))).
rewrite app_nil_r in H. apply H. rewrite rev_length.
clear. revert v; induction v; simpl; auto. }
apply Choice in C. destruct C as (phi, Hphi). clear H.
assert (Hphi' : forall genv v,
interp_form mo genv (phi v :: rev (Vector.to_list v)) A).
{ intros genv' v. rewrite interp_form_ext; eauto.
intros. clear - H Thm. destruct Thm as ((_ & _ & FA),_).
apply nForall_fclosed in FA. red in FA. cbn in FA.
now destruct (FA v0). }
set (mo' := Skolem_model_ext A f n E Thm M mo phi Hphi').
assert (ok' : interp_form mo' genv [] T).
{ eapply validity_theorem; eauto. red; auto. }
rewrite interp_form_skolem_premodel_ext; eauto.
unfold mo' in ok'. unfold Skolem_model_ext in ok'. cbn in ok'.
apply ok'.
Qed.
End SkolemTheorem.
(*
Check Skolem_consext.
Print Assumptions Skolem_consext.
*)
......@@ -21,5 +21,6 @@ PreModels.v
Models.v
Peano.v
ZF.v
Skolem.v
# parser.v
# FormulaReader.v
\ No newline at end of file
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment