Commit 202004fd authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Skolem: nprod instead of Vector

parent afd28b66
......@@ -4,7 +4,6 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Vector.
Require Export List NaryFunctions.
Import ListNotations.
......@@ -48,6 +47,9 @@ Definition optnapply {A B}(f:optnfun A B)(l:list A)(dft:B) :=
end.
Arguments nfun_to_nfun {A B C} f {n}.
Arguments ncurry {A B n}.
Arguments nuncurry {A B n}.
Arguments nprod_to_list {A n}.
Lemma build_args_ntn {A B B' n} (l : list A)(f:B->B')(any:B)(any':B') :
length l = n ->
......@@ -57,42 +59,30 @@ Proof.
intros <-. induction l; simpl; auto.
Qed.
(** See also nprod *)
(** 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 Open Scope vector_scope.
Fixpoint uncurry {n} : (A^^n-->B) -> Vector.t 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} : (Vector.t A n -> B) -> (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 to_nprod {A} n (l:list A) :
length l = n -> exists v : A^n, nprod_to_list v = l.
Proof.
intros <-.
exists (nprod_of_list _ l). induction l; cbn; f_equal; auto.
Qed.
Lemma uncurry_curry n (phi : Vector.t A n -> B) v :
uncurry (curry phi) v = phi v.
Lemma nprod_to_list_length {A} n (v:A^n) :
length (nprod_to_list v) = n.
Proof.
induction v; cbn; auto. now rewrite IHv.
induction n; cbn; auto. destruct v; cbn; auto.
Qed.
Lemma to_vect n (l:list A) :
length l = n -> exists v : Vector.t A n, Vector.to_list v = l.
Lemma build_args_nprod {A B} n (v:A^n) (f:A^^n-->B) (dft:B) :
build_args (nprod_to_list v) dft f = nuncurry f v.
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.
induction n; cbn in *; auto.
destruct v as (a,v). apply IHn.
Qed.
End Curry.
Lemma nuncurry_ncurry {A B n} (f : A^n->B) (v:A^n) :
nuncurry (ncurry f) v = f v.
Proof.
induction n; cbn in *; auto.
- now destruct v.
- destruct v as (a,v). now rewrite IHn.
Qed.
......@@ -206,20 +206,20 @@ Proof.
now destruct (funs mo f).
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 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.
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) :
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 (curry phi)) genv [] A0.
interp_form (Skolem_premodel_ext th M mo f n (ncurry phi)) genv [] A0.
Proof.
set (th' := Skolem_ext _ _ _ _ _ _) in *.
set (Phi := curry phi).
set (Phi := ncurry phi).
set (mo' := Skolem_premodel_ext _ _ _ _ _ _).
intros A0 [ | -> ] genv.
- unfold th'. simpl.
......@@ -231,7 +231,7 @@ intros A0 [ | -> ] genv.
destruct stk as [|m l]; try easy.
injection H as H.
rewrite <- rev_length in H.
destruct (to_vect _ _ H) as (v & Hv).
destruct (to_nprod _ _ 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.
......@@ -242,18 +242,18 @@ intros A0 [ | -> ] genv.
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). cbn. induction v; cbn; auto.
rewrite <- (nuncurry_ncurry phi v). cbn. apply build_args_nprod.
+ 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) :
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 (curry phi))).
apply (Build_Model _ th' (Skolem_premodel_ext th M mo f n (ncurry phi))).
apply Skolem_model_AxOk; auto.
Defined.
......@@ -280,15 +280,15 @@ Proof.
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).
assert (C : forall (v : M^n), exists m,
interp_form mo genv (m::rev (nprod_to_list v)) A).
{ intros v.
specialize (H (rev (Vector.to_list v))).
specialize (H (rev (nprod_to_list v))).
rewrite app_nil_r in H. apply H. rewrite rev_length.
clear. revert v; induction v; simpl; auto. }
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 (Vector.to_list v)) A).
interp_form mo genv (phi v :: rev (nprod_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.
......
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