PreModels : many improvements

Models.v

@@ -14,12 +14,12 @@ Local Open Scope eqb_scope.
 Record Model (M:Type)(th : theory) :=
  { pre :> PreModel M th;
    AxOk : forall A, IsAxiom th A ->
-                    forall G, interp_form pre G [] A }.
+                    forall G, finterp pre G [] A }.
 
 Lemma validity_theorem logic th :
  CoqRequirements logic ->
  forall T, IsTheorem logic th T ->
- forall M (mo : Model M th) G, interp_form mo G [] T.
+ forall M (mo : Model M th) G, finterp mo G [] T.
 Proof.
  intros CR T Thm M mo G.
  rewrite thm_alt in Thm.
@@ -256,9 +256,9 @@ Qed.
 Lemma interp_pred p l :
  WF th (Pred p l) ->
  forall G,
-   interp_form mo G [] (Pred p l) <->
+   finterp mo G [] (Pred p l) <->
    IsTheorem K th
-     (Pred p (map (fun t => this (interp_term mo G [] t)) l)).
+     (Pred p (map (fun t => this (tinterp mo G [] t)) l)).
 Proof.
  rewrite Pred_WF. intros (E,F) G.
  cbn. unfold mkpreds. rewrite E.
@@ -271,9 +271,9 @@ Proof.
  apply optnprod_to_list in E'. fold M. now rewrite E', map_map.
 Qed.
 
-Lemma interp_term_carac t :
+Lemma tinterp_carac t :
  WF th t ->
- forall G, this (interp_term mo G [] t) = term_closure G t.
+ forall G, this (tinterp mo G [] t) = term_closure G t.
 Proof.
  induction t as [ | | f l IH] using term_ind'; cbn; auto.
  - now rewrite wf_iff.
@@ -292,11 +292,11 @@ Proof.
    revert x Hx. now apply Forall_forall.
 Qed.
 
-Lemma interp_term_carac' (t:term) G (W : WF th t) :
-  interp_term mo G [] t =
+Lemma tinterp_carac' (t:term) G (W : WF th t) :
+  tinterp mo G [] t =
   {| this := term_closure G t; closed := term_closure_wc' t G W |}.
 Proof.
- apply proof_irr. cbn. now apply interp_term_carac.
+ apply proof_irr. cbn. now apply tinterp_carac.
 Qed.
 
 Lemma Thm_Not A : WC th A ->
@@ -420,7 +420,7 @@ Proof.
 Qed.
 
 Lemma interp_carac f : WF th f ->
- forall G, interp_form mo G [] f <-> IsTheorem K th (closure G f).
+ forall G, finterp mo G [] f <-> IsTheorem K th (closure G f).
 Proof.
  induction f as [h IH f Hf] using height_ind. destruct f; intros W G.
  - clear IH Hf. cbn.
@@ -433,7 +433,7 @@ Proof.
    rewrite interp_pred; auto. simpl.
    unfold vmap, vmap_list.
    f_equiv. f_equiv. apply map_ext_iff. intros t Ht.
-   apply interp_term_carac. revert t Ht. apply Forall_forall.
+   apply tinterp_carac. revert t Ht. apply Forall_forall.
    now apply Pred_WF in W.
  - simpl. rewrite IH; auto with arith.
    symmetry. apply Thm_Not.
@@ -465,13 +465,13 @@ Proof.
          - apply Nat.le_0_r, level_bsubst; auto. }
        rewrite Thm_Not in Thm by (apply closure_wc; auto).
        rewrite <- IH in Thm; auto.
-       rewrite <- interp_form_bsubst0 in Thm; auto. destruct Thm. apply H.
+       rewrite <- finterp_bsubst0 in Thm; auto. destruct Thm. apply H.
      * apply thm_notexnot; auto. apply (closure_wc (∀f)); auto.
    + intros Thm (t,Ht).
-     rewrite interp_form_bsubst0 with (u:=t); auto.
+     rewrite finterp_bsubst0 with (u:=t); auto.
      2:{ apply term_wc_iff in Ht. apply Ht. }
      2:{ destruct (proj2 (term_wc_iff _ _) Ht) as (W',F').
-         rewrite (interp_term_carac' t G W').
+         rewrite (tinterp_carac' t G W').
          apply proof_irr. cbn. apply term_vmap_id. intros v.
          red in F'. intuition. }
      apply term_wc_iff in Ht.
@@ -479,11 +479,11 @@ Proof.
      * rewrite closure_bsubst by apply Ht. apply Thm_All_e; auto.
      * apply bsubst_WF; auto. apply Ht.
    + intros ((t,Ht),Int).
-     rewrite interp_form_bsubst0 with (u:=t) in Int; auto.
+     rewrite finterp_bsubst0 with (u:=t) in Int; auto.
      2:{ clear Int. apply term_wc_iff in Ht. apply Ht. }
      2:{ clear Int.
          destruct (proj2 (term_wc_iff _ _) Ht) as (W',F').
-         rewrite (interp_term_carac' t G W').
+         rewrite (tinterp_carac' t G W').
          apply proof_irr. cbn. apply term_vmap_id. intros v.
          red in F'. intuition. }
      apply term_wc_iff in Ht.
@@ -499,12 +499,12 @@ Proof.
      2:{ now rewrite height_bsubst. }
      2:{ apply bsubst_WF; auto. now apply Cst_WC. }
      exists {| this := Cst c; closed := Cst_wc th c Hc |}.
-     rewrite interp_form_bsubst0; eauto.
-     apply proof_irr. rewrite interp_term_carac; auto. now apply Cst_WC.
+     rewrite finterp_bsubst0; eauto.
+     apply proof_irr. rewrite tinterp_carac; auto. now apply Cst_WC.
 Qed.
 
 Lemma interp_carac_closed f genv : WC th f ->
- interp_form mo genv [] f <-> IsTheorem K th f.
+ finterp mo genv [] f <-> IsTheorem K th f.
 Proof.
  intros W.
  replace f with (closure genv f) at 2.
@@ -515,7 +515,7 @@ Qed.
 
 Lemma axioms_ok A :
   IsAxiom th A ->
-  forall genv, interp_form mo genv [] A.
+  forall genv, finterp mo genv [] A.
 Proof.
  intros HA genv. apply interp_carac_closed.
  apply WCAxiom; auto.
@@ -555,11 +555,11 @@ Proof.
    destruct (predsymbs sign' p); auto.
 Defined.
 
-Lemma interp_term_restrict sign sign' M
+Lemma tinterp_restrict sign sign' M
  (mo:PreModel M sign')(SE:SignExtend sign sign') :
  forall genv lenv t, check sign t = true ->
-  interp_term (premodel_restrict sign sign' M SE mo) genv lenv t =
-  interp_term mo genv lenv t.
+  tinterp (premodel_restrict sign sign' M SE mo) genv lenv t =
+  tinterp mo genv lenv t.
 Proof.
  induction t as [ | | f args IH ] using term_ind'; cbn; auto.
  destruct (funsymbs sign f); [|easy].
@@ -568,11 +568,11 @@ Proof.
  apply IH; auto. rewrite forallb_forall in F; auto.
 Qed.
 
-Lemma interp_form_restrict sign sign' M
+Lemma finterp_restrict sign sign' M
  (mo:PreModel M sign')(SE:SignExtend sign sign') :
  forall genv lenv f, check sign f = true ->
-  interp_form (premodel_restrict sign sign' M SE mo) genv lenv f <->
-  interp_form mo genv lenv f.
+  finterp (premodel_restrict sign sign' M SE mo) genv lenv f <->
+  finterp mo genv lenv f.
 Proof.
  intros genv lenv f; revert genv lenv.
  induction f; cbn; intros genv lenv Hf; f_equal;
@@ -580,7 +580,7 @@ Proof.
  - destruct (predsymbs sign p); [|easy].
    rewrite lazy_andb_iff in Hf. destruct Hf as (_,Hf).
    f_equiv. apply map_ext_iff. intros t Ht.
-   apply interp_term_restrict. rewrite forallb_forall in Hf; auto.
+   apply tinterp_restrict. rewrite forallb_forall in Hf; auto.
  - now rewrite IHf.
  - destruct o; simpl; rewrite IHf1, IHf2; intuition.
  - destruct q; simpl; split.
@@ -597,7 +597,7 @@ Proof.
  intros CR (SE,EX) mo.
  apply Build_Model with (premodel_restrict th th' M SE mo).
  intros A HA genv.
- rewrite interp_form_restrict by (apply WCAxiom; auto).
+ rewrite finterp_restrict by (apply WCAxiom; auto).
  assert (Thm : IsTheorem logic th' A).
  { apply EX, ax_thm; auto. }
  apply (validity_theorem logic th' CR A Thm M mo).
@@ -626,7 +626,7 @@ Lemma completeness_theorem (th:theory) (nc : NewCsts th) :
  (forall A, A\/~A) ->
  forall T,
    WC th T ->
-   (forall M (mo : Model M th) genv, interp_form mo genv [] T)
+   (forall M (mo : Model M th) genv, finterp mo genv [] T)
    -> IsTheorem K th T.
 Proof.
  intros EM T WF HT.
@@ -663,11 +663,11 @@ Proof.
    - intros B HB. apply ax_thm. cbn. now right. }
  set (mo' := model_restrict K th th' M EM EX mo).
  set (genv := fun (_:variable) => mo.(someone)).
- assert (interp_form mo genv [] (~T)).
+ assert (finterp mo genv [] (~T)).
  { apply AxOk. cbn. now left. }
  cbn in H. apply H. clear H.
  set (SE := let (p,_) := EX in p).
- assert (U := interp_form_restrict th th' M mo SE genv [] T).
+ assert (U := finterp_restrict th th' M mo SE genv [] T).
  change (sign th') with (sign th) in U at 2.
  rewrite <- U by (apply WF).
  assert (E : pre _ _ mo' = premodel_restrict th th' M SE mo).

Peano.v

@@ -407,13 +407,13 @@ Definition PeanoPreModel : PreModel nat PeanoTheory :=
 
 Lemma PeanoAxOk A :
   IsAxiom PeanoTheory A ->
-  forall genv, interp_form PeanoPreModel genv [] A.
+  forall G, finterp PeanoPreModel G [] A.
 Proof.
  unfold PeanoTheory. simpl.
  unfold PeanoAx.IsAx.
  intros [IN|(B & -> & CK & CL)].
  - compute in IN. intuition; subst; cbn; intros; subst; omega.
- - intros genv.
+ - intros G.
    unfold PeanoAx.induction_schema.
    apply interp_nforall.
    intros stk Len. rewrite app_nil_r. cbn.
@@ -421,9 +421,9 @@ Proof.
    (* The Peano induction emulated by a Coq induction :-) *)
    induction m.
    + specialize (Base 0).
-     apply -> interp_form_bsubst_gen in Base; simpl; eauto.
+     apply -> finterp_bsubst_gen in Base; simpl; eauto.
    + apply Step in IHm.
-     apply -> interp_form_bsubst_gen in IHm; simpl; eauto.
+     apply -> finterp_bsubst_gen in IHm; simpl; eauto.
      now intros [|k].
 Qed.
 

Skolem.v

@@ -53,9 +53,9 @@ Proof.
  destruct n. auto. rewrite level_downvars; auto.
 Qed.
 
-Lemma interp_downvars sign M (mo:PreModel M sign) genv n l m :
+Lemma interp_downvars sign M (mo:PreModel M sign) G n l m :
  length l = n ->
- map (interp_term mo genv (m :: l)) (downvars n) = rev l.
+ map (tinterp mo G (m :: l)) (downvars n) = rev l.
 Proof.
  intros E.
  rewrite downvars_alt, map_rev. f_equal.
@@ -75,12 +75,11 @@ Definition Skolem_sign sign f n :=
    (fun funs s => if s =? f then Some n else funs s).
 
 Lemma Skolem_signext sign f n :
- sign.(funsymbs) f = None ->
+ funsymbs sign 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.
+ split; intro s; red; cbn; auto. case eqbspec; intros; subst; auto.
 Qed.
 
 (** The Skolem axiom for formula A, new symbol f of arity n.
@@ -115,7 +114,7 @@ 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 ->
+ funsymbs th f = None ->
  IsTheorem K th (nForall n (∃A)) ->
  forall B, SkolemAx th.(IsAxiom) A f n B -> WC (Skolem_sign th f n) B.
 Proof.
@@ -127,7 +126,7 @@ Proof.
 Qed.
 
 Definition Skolem_ext th A f n
- (E:th.(funsymbs) f = None)
+ (E:funsymbs th f = None)
  (Thm:IsTheorem K th (nForall n (∃A))) :=
  {| sign := Skolem_sign th f n;
     IsAxiom := SkolemAx th.(IsAxiom) A f n;
@@ -140,7 +139,7 @@ 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)
+Definition Skolem_premodel {sign M} (mo:PreModel M sign)
  f n (phi : M^^n-->M) : PreModel M (Skolem_sign sign f n).
 Proof.
 set (sign' := Skolem_sign _ _ _).
@@ -150,89 +149,42 @@ eapply (Build_PreModel sign' (someone mo) funs' (preds mo)); intros s.
 - 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 = Nop \/ 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).
+Lemma Skolem_premodelext sign M (mo:PreModel M sign) f n phi :
+ funsymbs sign f = None ->
+ PreModelExtend mo (Skolem_premodel mo f n phi).
 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 lazy_andb_iff. intros (_ & F) genv lenv.
-     destruct (FU f) as [Hf|Hf].
-     + exfalso. now rewrite (funsOk mo f), Hf in E.
-     + rewrite <- Hf. f_equiv; auto.
-       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 lazy_andb_iff. intros (_ & F) genv lenv.
-   rewrite <- PR. 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 lazy_andb_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: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).
+ intro H. constructor; auto; intro s; red; cbn; auto.
+ case eqbspec; auto. intros ->. left.
+ generalize (funsOk mo f). rewrite H. now destruct funs.
 Qed.
 
 Definition interp_phi {n th M} (mo:Model M th)(phi : M^n -> M) A :=
- forall genv v, interp_form mo genv (phi v :: rev (nprod_to_list v)) A.
+ forall G v, finterp mo G (phi v :: rev (nprod_to_list v)) A.
 
 Definition Skolem_model_AxOk A f n
- (E:th.(funsymbs) f = None)
+ (E:funsymbs th f = None)
  (Thm:IsTheorem K th (nForall n (∃A)))
  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 genv : variable -> M,
-  interp_form (Skolem_premodel_ext th M mo f n (ncurry phi)) genv [] A0.
+  forall G, finterp (Skolem_premodel mo f n (ncurry phi)) G [] A0.
 Proof.
 set (th' := Skolem_ext _ _ _ _ _ _) in *.
 set (Phi := ncurry 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 WCAxiom.
+set (mo' := Skolem_premodel _ _ _ _).
+assert (Hmo' := Skolem_premodelext _ _ mo f n Phi E).
+intros Ax [ | -> ] G.
+- rewrite <- finterp_premodelext; try exact Hmo'.
+  now apply AxOk. now apply WCAxiom.
 - unfold Skolem_axiom.
   rewrite interp_nforall. intros. rewrite app_nil_r.
   destruct stk as [|m l]; try easy.
   injection H as H.
   destruct (optnprod n (rev l)) as [v|] eqn:Ev.
   2:{ exfalso. revert Ev. apply optnprod_some. now rewrite rev_length. }
-  rewrite interp_form_bsubst_gen with (lenv' := phi v :: l); auto.
+  rewrite finterp_bsubst_gen with (L' := phi v :: l); auto.
   + unfold th'. simpl.
-    rewrite <- (interp_form_skolem_premodel_ext th M f n Phi mo); auto.
+    rewrite <- finterp_premodelext; try exact Hmo'.
     * apply optnprod_to_list in Ev.
       rewrite <- (rev_involutive l), <- Ev. apply Hphi.
     * clear -Thm. destruct Thm as (((CA,_),_),_).
@@ -245,19 +197,16 @@ intros A0 [ | -> ] genv.
   + destruct k; try easy.
 Qed.
 
-Definition Skolem_model_ext A f n
- (E:th.(funsymbs) f = None)
+Definition Skolem_model A f n
+ (E:funsymbs th f = None)
  (Thm:IsTheorem K th (nForall n (∃A)))
  M (mo:Model M th)(phi : 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 (ncurry phi))).
-apply Skolem_model_AxOk; auto.
-Defined.
+ Model M (Skolem_ext th A f n E Thm) :=
+ {| pre := _;
+    AxOk := Skolem_model_AxOk A f n E Thm M mo phi Hphi |}.
 
 Lemma Skolem_consext A f n
- (E:th.(funsymbs) f = None)
+ (E:funsymbs th f = None)
  (Thm:IsTheorem K th (nForall n (∃A))) :
  ConservativeExt K th (Skolem_ext th A f n E Thm).
 Proof.
@@ -274,30 +223,29 @@ Proof.
  - intros T HT CT.
    apply completeness_theorem; auto.
    + eapply WC_new_sign; auto. apply HT.
-   + intros M mo genv.
+   + intros M mo G.
      set (th' := Skolem_ext _ _ _ _ _ _) in *.
-     assert (interp_form mo genv [] (nForall n (∃ A))).
+     assert (finterp mo G [] (nForall n (∃ A))).
      { eapply validity_theorem; eauto. red; auto. }
      rewrite interp_nforall in H.
      assert (C : forall (v : M^n), exists m,
-                  interp_form mo genv (m::rev (nprod_to_list v)) A).
+                  finterp mo G (m::rev (nprod_to_list v)) A).
      { intros v.
        specialize (H (rev (nprod_to_list v))).
        rewrite app_nil_r in H. apply H. rewrite rev_length.
        apply nprod_to_list_length. }
      apply Choice in C. destruct C as (phi, Hphi). clear H.
-     assert (Hphi' : forall genv v,
-                interp_form mo genv (phi v :: rev (nprod_to_list v)) A).
-     { intros genv' v. rewrite interp_form_ext; eauto.
+     assert (Hphi' : forall G v,
+                finterp mo G (phi v :: rev (nprod_to_list v)) A).
+     { intros G' v. rewrite finterp_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).
+     set (mo' := Skolem_model A f n E Thm M mo phi Hphi').
+     assert (ok' : finterp mo' G [] 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'.
+     revert ok'. apply finterp_premodelext with (mo := mo); auto.
+     now apply Skolem_premodelext.
 Qed.
 End SkolemTheorem.