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

New file Wellfounded.v, WF is now just check+BClosed, earlier WF is now WC

 NB : WC stands for WellFormed+Closed, here Closed in the sense "no free variables",
 i.e. FVars

 Also: some class overloading for fclosed, etc etc
parent 368c5443
......@@ -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 Nary.v PreModels.v Models.v Peano.v contribs/zfc/zfc.v ZF.v Skolem.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 Wellformed.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v Nary.v PreModels.v Models.v Peano.v contribs/zfc/zfc.v ZF.v Skolem.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
......
......@@ -1035,6 +1035,22 @@ Proof.
intro. cbn. intuition.
Qed.
Lemma Pr_app_l logic Γ Δ A :
Pr logic (Γ A) ->
Pr logic (Γ++Δ A).
Proof.
intros. eapply Pr_weakening; eauto. constructor. intro.
rewrite in_app_iff. now left.
Qed.
Lemma Pr_app_r logic Γ Δ A :
Pr logic (Δ A) ->
Pr logic (Γ++Δ A).
Proof.
intros. eapply Pr_weakening; eauto. constructor. intro.
rewrite in_app_iff. now right.
Qed.
Lemma Valid_pop logic A B Γ d :
Valid logic d -> Claim d (Γ A) ->
let d' := subset_deriv (B::Γ) d in
......@@ -1333,9 +1349,9 @@ Proof.
+ apply R_And_e1 with (B := f1). apply R_Ax. apply in_eq.
Qed.
(** Properties of [term_fclosed] and [form_fclosed] *)
(** Properties of [fclosed] *)
Lemma term_fclosed_spec t : term_fclosed t = true <-> FClosed t.
Lemma term_fclosed_spec t : fclosed t = true <-> FClosed t.
Proof.
unfold FClosed.
induction t using term_ind'; cbn.
......@@ -1349,7 +1365,7 @@ Proof.
now exists x.
Qed.
Lemma form_fclosed_spec f : form_fclosed f = true <-> FClosed f.
Lemma form_fclosed_spec f : fclosed f = true <-> FClosed f.
Proof.
unfold FClosed.
induction f; cbn; auto.
......@@ -1361,7 +1377,7 @@ Proof.
Qed.
Lemma fclosed_bsubst n t f :
term_fclosed t = true -> form_fclosed (bsubst n t f) = form_fclosed f.
fclosed t = true -> fclosed (bsubst n t f) = fclosed f.
Proof.
intros E. apply eq_true_iff_eq. rewrite !form_fclosed_spec.
rewrite term_fclosed_spec in E. unfold FClosed in *.
......@@ -1371,8 +1387,7 @@ Proof.
now rewrite H.
Qed.
Lemma fclosed_lift_above n f :
form_fclosed (lift n f) = form_fclosed f.
Lemma fclosed_lift n f : fclosed (lift n f) = fclosed f.
Proof.
apply eq_true_iff_eq. rewrite !form_fclosed_spec.
unfold FClosed. now rewrite fvars_lift_form.
......
......@@ -958,17 +958,22 @@ Qed.
(** A direct boolean version of [FClosed], easier to use than
[Names.is_empty (fvars ...)] *)
Fixpoint term_fclosed t :=
Class IsFClosed (A : Type) := fclosed : A -> bool.
Arguments fclosed {_} {_} !_.
Instance term_fclosed : IsFClosed term :=
fix term_fclosed t :=
match t with
| BVar _ => true
| FVar _ => false
| Fun _ l => forallb term_fclosed l
end.
Fixpoint form_fclosed f :=
Instance form_fclosed : IsFClosed formula :=
fix form_fclosed f :=
match f with
| True | False => true
| Pred _ l => forallb term_fclosed l
| Pred _ l => forallb fclosed l
| Not f => form_fclosed f
| Op _ f1 f2 => form_fclosed f1 &&& form_fclosed f2
| Quant _ f => form_fclosed f
......
This diff is collapsed.
......@@ -47,17 +47,12 @@ Definition optnapply {A B}(f:optnfun A B)(l:list A)(dft:B) :=
| Nop => dft
end.
(** See also nfun_to_nfun *)
Fixpoint map_arity {A B B' n}(f:B->B') : A^^n-->B -> A^^n-->B' :=
match n with
| 0 => f
| S n => fun ab a => map_arity f (ab a)
end.
Arguments nfun_to_nfun {A B C} f {n}.
Lemma build_map_arity {A B B' n} (l : list A)(f:B->B')(any:B)(any':B') :
Lemma build_args_ntn {A B B' n} (l : list A)(f:B->B')(any:B)(any':B') :
length l = n ->
forall (a : A^^n-->B),
build_args l any' (map_arity f a) = f (build_args l any a).
build_args l any' (nfun_to_nfun f a) = f (build_args l any a).
Proof.
intros <-. induction l; simpl; auto.
Qed.
......
......@@ -4,7 +4,8 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Mix Meta Theories Nary PreModels Models.
Require Import Defs NameProofs Mix Meta.
Require Import Wellformed Theories Nary PreModels Models.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope string_scope.
......@@ -67,12 +68,10 @@ Definition IsAx A :=
check PeanoSign B = true /\
FClosed B.
Lemma WfAx A : IsAx A -> Wf PeanoSign A.
Lemma WCAx A : IsAx A -> WC PeanoSign A.
Proof.
intros [ IN | (B & -> & HB & HB')].
- apply Wf_iff.
unfold axioms_list in IN.
simpl in IN. intuition; subst; reflexivity.
- apply wc_iff. revert A IN. now apply forallb_forall.
- repeat split; unfold induction_schema; cbn.
+ rewrite nForall_check. cbn.
rewrite !check_bsubst, HB; auto.
......@@ -93,7 +92,7 @@ Local Open Scope formula_scope.
Definition PeanoTheory :=
{| sign := PeanoSign;
IsAxiom := PeanoAx.IsAx;
WfAxiom := PeanoAx.WfAx |}.
WCAxiom := PeanoAx.WCAx |}.
(** Useful lemmas so as to be able to write proofs that take less than 1000 lines. *)
......@@ -265,7 +264,7 @@ Ltac hered := apply AntiHereditarity; calc.
Ltac trans b := apply Transitivity with (B := b); calc.
Ltac thm := unfold IsTheorem; split; [ unfold Wf; split; [ auto | split; auto ] | ].
Ltac thm := unfold IsTheorem; split; [ now apply wc_iff | ].
Ltac parse term :=
match term with
......
......@@ -7,7 +7,7 @@
Require Import ChoiceFacts.
Require Import Defs NameProofs Mix Meta.
Require Import Theories NaryFunctions Nary PreModels Models.
Require Import Wellformed Theories NaryFunctions Nary PreModels Models.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope eqb_scope.
......@@ -92,13 +92,13 @@ Qed.
Definition Skolem_axiom A f n :=
nForall (S n) (bsubst 0 (Fun f (downvars n)) A).
Lemma Skolem_axiom_wf sign f n A :
Lemma Skolem_axiom_wc sign f n A :
funsymbs sign f = Some n ->
Wf sign (nForall n ( A)) ->
Wf sign (Skolem_axiom A f n).
WC sign (nForall n ( A)) ->
WC sign (Skolem_axiom A f n).
Proof.
unfold Skolem_axiom.
intros Hf (CA & LA & FA). repeat split.
intros Hf ((CA & LA) & FA). repeat split.
- rewrite nForall_check, check_bsubst in *; auto.
cbn. rewrite Hf.
clear. induction n; simpl; auto.
......@@ -119,13 +119,13 @@ Definition SkolemAx Ax (A:formula) 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.
forall B, SkolemAx th.(IsAxiom) A f n B -> WC (Skolem_sign th f n) B.
Proof.
intros Hc (CL & _) B [HB| -> ].
- eauto using signext_wf, Skolem_signext, WfAxiom.
- apply Skolem_axiom_wf.
intros Hc (W,_) B [HB| -> ].
- eauto using signext_wc, Skolem_signext, WCAxiom.
- apply Skolem_axiom_wc.
+ simpl. now rewrite eqb_refl.
+ eauto using signext_wf, Skolem_signext.
+ eauto using signext_wc, Skolem_signext.
Qed.
Definition Skolem_ext th A f n
......@@ -133,7 +133,7 @@ Definition Skolem_ext th A f n
(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 |}.
WCAxiom := SkolemAxWf th A f n E Thm |}.
Section SkolemTheorem.
Variable EM : forall A:Prop, A\/~A.
......@@ -225,7 +225,7 @@ 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.
+ now apply WCAxiom.
- unfold Skolem_axiom.
rewrite interp_nforall. intros. rewrite app_nil_r.
destruct stk as [|m l]; try easy.
......@@ -236,7 +236,7 @@ intros A0 [ | -> ] genv.
+ 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 & _ & _),_).
* clear -Thm. destruct Thm as (((CA,_),_),_).
rewrite nForall_check in CA. apply CA.
+ simpl nth_error. f_equal.
cbn. rewrite eqb_refl.
......@@ -267,14 +267,14 @@ Proof.
- rewrite extend_alt. split.
+ now apply Skolem_signext.
+ intros B HB. split.
* apply signext_wf with th.
* apply signext_wc with th.
now apply Skolem_signext.
now apply WfAxiom.
now apply WCAxiom.
* exists [B]. split. constructor; auto. simpl. red. now left.
apply R'_Ax.
- intros T HT CT.
apply completeness_theorem; auto.
+ split; auto. apply HT.
+ eapply WC_new_sign; auto. apply HT.
+ intros M mo genv.
set (th' := Skolem_ext _ _ _ _ _ _) in *.
assert (interp_form mo genv [] (nForall n ( A))).
......@@ -290,7 +290,7 @@ Proof.
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),_).
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').
......
This diff is collapsed.
......@@ -81,6 +81,12 @@ Qed.
(** List stuff *)
Lemma Forall_app A (P:A->Prop) (l l':list A) :
Forall P (l++l') <-> Forall P l /\ Forall P l'.
Proof.
rewrite !Forall_forall. setoid_rewrite in_app_iff. firstorder.
Qed.
Fixpoint list_assoc {A B}`{Eqb A} x (l:list (A*B)) :=
match l with
| [] => None
......
(** * Well-formed terms and formulas *)
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs Mix Meta.
Local Open Scope bool_scope.
Local Open Scope eqb_scope.
(** Well-formed terms and formulas over a particular signature :
- use only the symbols of this signature
- with the correct arity
- and moreover with bounded variables that are indeed bounded.
Thanks to class overloading, [WF] also works for contexts, sequents,
derivations...
Note that a derivation which is not well-formed may still be valid
(in the sense of [Mix.Valid] or [Mix.Pr]). We'll see in [Restrict.v]
how we can force the inners of a derivation to be well-formed.
*)
Definition WF {T}`{Check T}`{Level T} sign (t:T) :=
check sign t = true /\ BClosed t.
Definition wf {T}`{Check T}`{Level T} sign (t:T) :=
check sign t && (level t =? 0).
(** By default, the second arguments of [WF] are to be parsed as formula. *)
Arguments WF {T _ _} sign t%form.
Arguments wf {T _ _} sign t%form.
Lemma wf_spec {T}`{Check T}`{Level T} sign (t:T) :
reflect (WF sign t) (wf sign t).
Proof.
unfold WF, wf, BClosed.
destruct check; cbn; [case eqbspec|]; now constructor.
Qed.
Lemma wf_iff {T}`{Check T}`{Level T} sign (t:T) :
WF sign t <-> wf sign t = true.
Proof.
apply reflect_iff, wf_spec.
Qed.
Lemma Op_WF sign o A B :
WF sign (Op o A B) <-> WF sign A /\ WF sign B.
Proof.
unfold WF, BClosed. cbn.
rewrite lazy_andb_iff. rewrite max_0. intuition.
Qed.
Lemma Fun_WF sign f l :
WF sign (Fun f l) <->
sign.(funsymbs) f = Some (length l) /\ Forall (WF sign) l.
Proof.
unfold WF, BClosed.
rewrite Forall_forall. cbn.
destruct funsymbs as [a|]; [|easy]. rewrite lazy_andb_iff.
rewrite list_max_map_0, forallb_forall, eqb_eq.
firstorder. congruence.
Qed.
Lemma Pred_WF sign p l :
WF sign (Pred p l) <->
sign.(predsymbs) p = Some (length l) /\ Forall (WF sign) l.
Proof.
unfold WF, BClosed.
rewrite Forall_forall. cbn.
destruct predsymbs as [a|]; [|easy]. rewrite lazy_andb_iff.
rewrite list_max_map_0, forallb_forall, eqb_eq.
firstorder. congruence.
Qed.
Lemma bsubst_WF sign A t :
WF sign (A) -> WF sign t -> WF sign (bsubst 0 t A).
Proof.
intros (CK,BC) (CK',BC'). split.
- apply check_bsubst; auto.
- apply Nat.le_0_r.
apply level_bsubst; red in BC; red in BC'; cbn in *; omega.
Qed.
Lemma cons_WF sign f (c:context) :
WF sign (f::c) <-> WF sign f /\ WF sign c.
Proof.
unfold WF, BClosed. cbn.
rewrite max_0, !andb_true_iff. intuition.
Qed.
Lemma ctx_WF sign (c:context) : WF sign c <-> Forall (WF sign) c.
Proof.
induction c.
- now unfold WF, BClosed.
- rewrite cons_WF, IHc. split; auto.
now constructor. inversion 1; subst; auto.
Qed.
Lemma seq_WF sign f (c:context) :
WF sign (c f) <-> WF sign c /\ WF sign f.
Proof.
unfold WF, BClosed. cbn. rewrite max_0, lazy_andb_iff. intuition.
Qed.
(** WC : Well-formed Closed terms and formulas are moreover without
free variables. See in particular axioms and theorems in [Theory.v],
and points of the syntactic model in [Model.v]. *)
Definition WC {T}`{Check T}`{Level T}`{FVars T} sign (t:T) :=
WF sign t /\ FClosed t.
Definition wc {T}`{Check T}`{Level T}`{IsFClosed T} sign (t:T) :=
wf sign t && fclosed t.
Hint Unfold WF WC.
Arguments WC {T _ _ _} sign t%form.
Arguments wc {T _ _ _} sign t%form.
Implicit Types t : term.
Implicit Types A : formula.
Lemma term_wc_spec sign t : reflect (WC sign t) (wc sign t).
Proof.
unfold WC, wc.
case wf_spec; cbn; [ | now constructor].
destruct (fclosed t) eqn:E.
- rewrite term_fclosed_spec in E. now constructor.
- constructor. rewrite <- term_fclosed_spec, E. easy.
Qed.
Lemma term_wc_iff sign t : WC sign t <-> wc sign t = true.
Proof.
apply reflect_iff, term_wc_spec.
Qed.
Lemma wc_spec sign A : reflect (WC sign A) (wc sign A).
Proof.
unfold WC, wc.
case wf_spec; cbn; [ | now constructor].
destruct (fclosed A) eqn:E.
- rewrite form_fclosed_spec in E. now constructor.
- constructor. rewrite <- form_fclosed_spec, E. easy.
Qed.
Lemma wc_iff sign A : WC sign A <-> wc sign A = true.
Proof.
apply reflect_iff, wc_spec.
Qed.
Lemma WC_dec sign A : { WC sign A }+{ ~WC sign A }.
Proof.
destruct (wc sign A) eqn:E; [left|right].
- now apply wc_iff.
- now rewrite wc_iff, E.
Qed.
Lemma True_WC sign : WC sign True.
Proof.
now rewrite wc_iff.
Qed.
Lemma False_WC sign : WC sign False.
Proof.
now rewrite wc_iff.
Qed.
Lemma Not_WC sign A : WC sign (Not A) <-> WC sign A.
Proof.
now rewrite !wc_iff.
Qed.
Lemma Op_WC sign o A B :
WC sign (Op o A B) <-> WC sign A /\ WC sign B.
Proof.
unfold WC, FClosed. cbn. rewrite Op_WF; intuition.
Qed.
Lemma bsubst_cst_WC sign c A :
sign.(funsymbs) c = Some 0 ->
WC sign (A) -> WC sign (bsubst 0 (Cst c) A).
Proof.
intros E ((CK,BC),FC).
repeat split; unfold BClosed in *; cbn in *.
- rewrite check_bsubst; auto. cbn. now rewrite E, eqb_refl.
- apply Nat.le_0_r, level_bsubst; auto with *.
- rewrite <- !form_fclosed_spec in *. now rewrite fclosed_bsubst.
Qed.
Lemma Fun_WC sign f l :
WC sign (Fun f l) <->
sign.(funsymbs) f = Some (length l) /\ Forall (WC sign) l.
Proof.
unfold WC. rewrite Fun_WF.
rewrite <- term_fclosed_spec. cbn.
rewrite forallb_forall, !Forall_forall.
setoid_rewrite term_fclosed_spec. intuition.
now apply H1. now apply H1.
Qed.
Lemma Pred_WC sign p l :
WC sign (Pred p l) <->
sign.(predsymbs) p = Some (length l) /\ Forall (WC sign) l.
Proof.
unfold WC. rewrite Pred_WF.
rewrite <- form_fclosed_spec. cbn.
rewrite forallb_forall, !Forall_forall.
setoid_rewrite term_fclosed_spec. intuition.
now apply H1. now apply H1.
Qed.
Lemma Cst_WC sign c :
sign.(funsymbs) c = Some 0 -> WC sign (Cst c).
Proof.
intros. now apply Fun_WC.
Qed.
Lemma Cst_wc sign c :
sign.(funsymbs) c = Some 0 -> wc sign (Cst c) = true.
Proof.
rewrite <- term_wc_iff. apply Cst_WC.
Qed.
Lemma bsubst_WC sign A t :
WC sign (A) -> WC sign t -> WC sign (bsubst 0 t A).
Proof.
intros (W,F) (W',F'). split.
- now apply bsubst_WF.
- rewrite <- form_fclosed_spec, fclosed_bsubst.
now rewrite form_fclosed_spec.
now rewrite term_fclosed_spec.
Qed.
Lemma WC_new_sign sign sign' A :
check sign' A = true -> WC sign A -> WC sign' A.
Proof.
now intros ? ((?,?),?).
Qed.
Lemma cons_WC sign f (c:context) :
WC sign (f::c) <-> WC sign f /\ WC sign c.
Proof.
unfold WC, FClosed. cbn -[Names.union].
rewrite cons_WF. intuition.
Qed.
Lemma ctx_WC sign (c:context) : WC sign c <-> Forall (WC sign) c.
Proof.
induction c.
- now unfold WC, FClosed.
- rewrite cons_WC, IHc. split; auto.
now constructor. inversion 1; subst; auto.
Qed.
Lemma seq_WC sign f (c:context) :
WC sign (c f) <-> WC sign c /\ WC sign f.
Proof.
unfold WC, FClosed. cbn. rewrite seq_WF. intuition.
Qed.
......@@ -3,7 +3,8 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs NameProofs Mix Meta Theories PreModels Models Peano.
Require Import Defs NameProofs Mix Meta.
Require Import Wellformed Theories PreModels Models Peano.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope eqb_scope.
......@@ -131,12 +132,10 @@ Proof.
symmetry. apply Nat.max_monotone. red. red. auto with *.
Qed.
Lemma WfAx A : IsAx A -> Wf ZFSign A.
Lemma WCAx A : IsAx A -> WC ZFSign A.
Proof.
intros [ IN | [ (B & -> & HB & HB') | (C & -> & HC & HC') ] ].
- apply Wf_iff.
unfold axioms_list in IN.
simpl in IN. intuition; subst; reflexivity.
- apply wc_iff. revert A IN. now apply forallb_forall.
- repeat split; unfold separation_schema; cbn.
+ rewrite nForall_check. cbn.
rewrite !check_lift_form, HB.
......@@ -148,7 +147,7 @@ Proof.
apply Nat.sub_0_le.
repeat apply Nat.max_lub; omega with *.
+ apply nForall_fclosed. rewrite <- form_fclosed_spec in *.
cbn. now rewrite fclosed_lift_above, HB'.
cbn. now rewrite fclosed_lift, HB'.
- repeat split; unfold replacement_schema; cbn.
+ rewrite nForall_check. cbn.
rewrite !check_lift_form, HC.
......@@ -161,7 +160,7 @@ Proof.
apply Nat.sub_0_le.
repeat apply Nat.max_lub; omega with *.
+ apply nForall_fclosed. rewrite <- form_fclosed_spec in *.
cbn. now rewrite !fclosed_lift_above, HC'.
cbn. now rewrite !fclosed_lift, HC'.
Qed.
End ZFAx.
......@@ -172,7 +171,7 @@ Local Open Scope formula_scope.
Definition ZF :=
{| sign := ZFSign;
IsAxiom := ZFAx.IsAx;
WfAxiom := ZFAx.WfAx |}.
WCAxiom := ZFAx.WCAx |}.
Import ZFAx.
......
......@@ -12,6 +12,7 @@ NameProofs.v
Subst.v
Restrict.v
Meta.v
Wellformed.v
Equiv.v
Equiv2.v
AltSubst.v
......
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