Commit 6c48f50d authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Shortcut : (interp mo A) is (forall G, finterp mo G [] A)

parent f9fecd84
......@@ -11,15 +11,22 @@ Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope eqb_scope.
(** We'll frequently consider interpretations of formulas over all
possible global environments, so here's a convenient shortcut *)
Definition interp {sign M} (mo : PreModel M sign) A :=
forall G, finterp mo G [] A.
(** A Model is a PreModel that satisfies all the axioms of the theory. *)
Record Model (M:Type)(th : theory) :=
{ pre :> PreModel M th;
AxOk : forall A, IsAxiom th A ->
forall G, finterp pre G [] A }.
AxOk : forall A, IsAxiom th A -> interp pre A }.
Lemma validity_theorem logic th :
CoqRequirements logic ->
forall T, IsTheorem logic th T ->
forall M (mo : Model M th) G, finterp mo G [] T.
forall M (mo : Model M th), interp mo T.
Proof.
intros CR T Thm M mo G.
rewrite thm_alt in Thm.
......@@ -513,9 +520,7 @@ Proof.
red in F. intuition.
Qed.
Lemma axioms_ok A :
IsAxiom th A ->
forall G, finterp mo G [] A.
Lemma axioms_ok A : IsAxiom th A -> interp mo A.
Proof.
intros HA G. apply interp_carac_closed.
apply WCAxiom; auto.
......
......@@ -406,15 +406,13 @@ Definition PeanoPreModel : PreModel nat PeanoTheory :=
predsOk := PeanoPreds_ok |}.
Lemma PeanoAxOk A :
IsAxiom PeanoTheory A ->
forall G, finterp PeanoPreModel G [] A.
IsAxiom PeanoTheory A -> interp PeanoPreModel A.
Proof.
unfold PeanoTheory. simpl.
unfold PeanoAx.IsAx.
intros [IN|(B & -> & CK & CL)].
intros [IN|(B & -> & CK & CL)] G.
- compute in IN. intuition; subst; cbn; intros; subst; omega.
- intros G.
unfold PeanoAx.induction_schema.
- unfold PeanoAx.induction_schema.
apply interp_nforall.
intros stk Len. rewrite app_nil_r. cbn.
intros (Base,Step).
......
......@@ -460,7 +460,7 @@ Qed.
Lemma tinterp_premodelext sg sg' M (mo:PreModel M sg) (mo':PreModel M sg') :
PreModelExtend mo mo' ->
forall t, check sg t = true ->
forall g l, tinterp mo g l t = tinterp mo' g l t.
forall G L, tinterp mo G L t = tinterp mo' G L t.
Proof.
intros (SO,SF,SP).
induction t as [ | | f l IH] using term_ind'; cbn.
......@@ -476,7 +476,7 @@ Qed.
Lemma finterp_premodelext sg sg' M (mo:PreModel M sg) (mo':PreModel M sg') :
PreModelExtend mo mo' ->
forall A, check sg A = true ->
forall g l, finterp mo g l A <-> finterp mo' g l A.
forall G L, finterp mo G L A <-> finterp mo' G L A.
Proof.
intros ME.
induction A; cbn.
......
......@@ -4,7 +4,6 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import ChoiceFacts.
Require Import Defs NameProofs Mix Meta.
Require Import Wellformed Theories NaryFunctions Nary PreModels Models.
......@@ -167,7 +166,7 @@ Definition Skolem_model_AxOk A f n
M (mo:Model M th)(phi : M^n -> M)(Hphi : interp_phi mo phi A) :
forall A0 : formula,
IsAxiom (Skolem_ext th A f n E Thm) A0 ->
forall G, finterp (Skolem_premodel mo f n (ncurry phi)) G [] A0.
interp (Skolem_premodel mo f n (ncurry phi)) A0.
Proof.
set (th' := Skolem_ext _ _ _ _ _ _) in *.
set (Phi := ncurry phi).
......
......@@ -598,11 +598,11 @@ Proof.
intros [|k]; cbn -[EQ]; auto with zfc.
Qed.
Lemma ZFAxOk A : IsAxiom ZF A -> forall G, finterp preZF G [] A.
Lemma ZFAxOk A : IsAxiom ZF A -> interp preZF A.
Proof.
unfold ZF. simpl.
unfold ZFAx.IsAx.
intros [HA|[(B & -> & CK & CL)|(B & -> & CK & CL)]].
intros [HA|[(B & -> & CK & CL)|(B & -> & CK & CL)]] G.
- unfold axioms_list in HA.
simpl in HA; intuition; subst; cbn -[EQ IN].
+ exact EQ_refl.
......@@ -616,7 +616,6 @@ Proof.
+ intros a. exists (Power a). apply Power_spec.
+ exists Omega. apply Omega_spec.
- (* separation *)
intros G.
unfold separation_schema.
apply interp_nforall. intros stk Len. rewrite app_nil_r. cbn.
setoid_rewrite finterp_lift. cbn.
......@@ -626,7 +625,7 @@ Proof.
{ intros u v E. apply finterp_zf_congr; auto.
destruct k; cbn -[EQ]; auto with zfc. }
- (* replacement *)
intros G. unfold replacement_schema.
unfold replacement_schema.
apply interp_nforall. intros stk Len. rewrite app_nil_r.
cbn -[exists_uniq].
setoid_rewrite finterp_lift. cbn -[exists_uniq].
......
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