Commit 312b061d authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

cleanup in Nary and Skolem

parent 6c48f50d
......@@ -29,18 +29,6 @@ Proof.
induction n; cbn; auto. destruct v; cbn; auto.
Qed.
Fixpoint nprod_map {A B} (f:A->B) {n} : A^n -> B^n :=
match n with
| 0 => fun _ => tt
| S n => fun '(a,v) => (f a, nprod_map f v)
end.
Lemma nprod_map_to_list {A B} (f:A->B) {n} (v:A^n) :
nprod_to_list (nprod_map f v) = map f (nprod_to_list v).
Proof.
induction n; cbn; destruct v; cbn; f_equal; auto.
Qed.
(** A variant of [nprod_of_list] with a precise size as target *)
Fixpoint optnprod {A} n (l:list A) : option (A^n) :=
......
......@@ -139,10 +139,10 @@ Variable th : theory.
Variable NC : NewCsts th.
Definition Skolem_premodel {sign M} (mo:PreModel M sign)
f n (phi : M^^n-->M) : PreModel M (Skolem_sign sign f n).
f n (phi : M^n->M) : PreModel M (Skolem_sign sign f n).
Proof.
set (sign' := Skolem_sign _ _ _).
set (funs' := fun s => if s =? f then NFun n phi else funs mo s).
set (funs' := fun s => if s =? f then NFun n (ncurry 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.
......@@ -166,12 +166,11 @@ 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 ->
interp (Skolem_premodel mo f n (ncurry phi)) A0.
interp (Skolem_premodel mo f n phi) A0.
Proof.
set (th' := Skolem_ext _ _ _ _ _ _) in *.
set (Phi := ncurry phi).
set (mo' := Skolem_premodel _ _ _ _).
assert (Hmo' := Skolem_premodelext _ _ mo f n Phi E).
assert (Hmo' := Skolem_premodelext _ _ mo f n phi E).
intros Ax [ | -> ] G.
- rewrite <- finterp_premodelext; try exact Hmo'.
now apply AxOk. now apply WCAxiom.
......@@ -191,8 +190,7 @@ intros Ax [ | -> ] G.
+ simpl nth_error. f_equal.
cbn. rewrite eqb_refl.
rewrite interp_downvars; auto.
unfold Phi. unfold napply_dft. cbn.
rewrite Ev. cbn. now rewrite nuncurry_ncurry.
unfold napply_dft. cbn. rewrite Ev. cbn. now rewrite nuncurry_ncurry.
+ destruct k; try easy.
Qed.
......
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