Commit 368c5443 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

new file Nary.v, start cleaning the use of dependent types such as NaryFunctions.nfun

parent c10bfa14
......@@ -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 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 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 =
......
......@@ -4,7 +4,8 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Eqdep_dec Defs Mix NameProofs Meta Theories PreModels.
Require Import Eqdep_dec Defs Mix NameProofs Meta.
Require Import Theories NaryFunctions Nary PreModels.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
......@@ -146,22 +147,6 @@ Proof.
rewrite UIP_refl_bool. apply UIP_refl_bool.
Qed.
Fixpoint map_arity {A B B'}(f:B->B') n
: arity_fun A n B -> arity_fun A n B' :=
match n with
| 0 => f
| S n => fun ab a => map_arity f n (ab a)
end.
Lemma build_map_arity {A B B'} n (l : list A)(f:B->B')(any:B)(any':B') :
length l = n ->
forall (a : arity_fun A n B),
build_args n l any' (map_arity f n a) =
f (build_args n l any a).
Proof.
intros <-. induction l; simpl; auto.
Qed.
Section SyntacticPreModel.
Variable logic : Defs.logic.
Variable th : theory.
......@@ -183,14 +168,14 @@ Qed.
Definition sized_wf_listterm n :=
{l : list term | length l = n /\ Forall (Wf_term th) l}.
Fixpoint mk_args n : arity_fun M n (sized_wf_listterm n) :=
Fixpoint mk_args n : M^^n --> sized_wf_listterm n :=
match n with
| 0 => exist _ [] (conj eq_refl (Forall_nil _))
| S n => fun t =>
map_arity (fun '(exist _ l Hl) =>
let '(exist _ t Ht) := t in
exist _ (t::l) (cons_ok t l n Ht Hl))
n (mk_args n)
(mk_args n)
end.
Definition one_listterm n : sized_wf_listterm n.
......@@ -203,7 +188,7 @@ Qed.
Lemma build_mk n (l : list M) (any:sized_wf_listterm n) :
length l = n ->
proj1_sig (build_args n l any (mk_args n)) =
proj1_sig (build_args l any (mk_args n)) =
map (@proj1_sig _ _) l.
Proof.
intros <-.
......@@ -215,7 +200,7 @@ Proof.
Qed.
Definition fun_core f n :
(th.(funsymbs) f = Some n) -> arity_fun M n M.
(th.(funsymbs) f = Some n) -> M^^n-->M.
Proof.
intros E.
generalize (mk_args n).
......@@ -224,28 +209,28 @@ Proof.
Defined.
Definition rich_funs f :
{ o : option { n:nat & arity_fun M n M } |
{ o : optnfun M M |
th.(funsymbs) f = get_arity o /\
match o with
| None => Logic.True
| Some (existT _ n a) =>
| Nop => Logic.True
| NFun n a =>
forall (l: list M)(any : M), length l = n ->
proj1_sig (build_args n l any a) =
proj1_sig (build_args l any a) =
Fun f (map (@proj1_sig _ _) l)
end }.
Proof.
destruct (th.(funsymbs) f) as [n|] eqn:E.
- set (r := fun_core f n E).
exists (Some (existT _ n r)); split; auto.
exists (NFun _ r); split; auto.
intros l any Hl.
unfold r, fun_core.
rewrite build_map_arity with (any0 := one_listterm n); auto.
rewrite <- (build_mk n l (one_listterm n) Hl).
destruct build_args. now cbn.
- now exists None.
- now exists Nop.
Defined.
Definition mk_funs : modfuns M :=
Definition mk_funs : string -> optnfun M M :=
fun f => proj1_sig (rich_funs f).
Lemma mk_funs_ok f : th.(funsymbs) f = get_arity (mk_funs f).
......@@ -253,15 +238,15 @@ Proof.
unfold mk_funs. now destruct (rich_funs f).
Qed.
Definition mk_preds : modpreds M.
Definition mk_preds : string -> optnfun M Prop.
Proof.
intro p.
destruct (th.(predsymbs) p) as [n|].
- apply Some. exists n.
- apply (NFun n).
generalize (mk_args n).
apply map_arity.
exact (fun sl => IsTheorem logic th (Pred p (proj1_sig sl))).
- apply None.
- apply Nop.
Defined.
Lemma mk_preds_ok p : th.(predsymbs) p = get_arity (mk_preds p).
......@@ -428,7 +413,7 @@ Proof.
unfold BClosed. cbn.
destruct (predsymbs th p) as [n|] eqn:E; [|easy].
rewrite lazy_andb_iff, eqb_eq. intros (L,CK) BC genv.
unfold mk_preds; rewrite E. clear E.
unfold mk_preds; rewrite E. cbn. clear E.
set (l0 := one_listterm th oneconst Honeconst n).
rewrite build_map_arity with (any := l0) by now rewrite map_length.
rewrite build_mk with (oneconst := oneconst) by (auto; now rewrite map_length).
......@@ -446,7 +431,7 @@ Proof.
rewrite lazy_andb_iff, eqb_eq.
intros (L,CK) BC genv.
unfold mk_funs.
destruct rich_funs as ([(n',a)| ] & Ho & Ho'); cbn in *.
destruct rich_funs as ([n' a| ] & Ho & Ho'); cbn in *.
2: congruence.
assert (Hn : n' = n) by congruence.
subst n'.
......@@ -796,11 +781,11 @@ Lemma premodel_restrict sign sign' M :
Proof.
intros SE mo.
set (fs := fun f => match sign.(funsymbs) f with
| None => None
| None => Nop
| _ => mo.(funs) f
end).
set (ps := fun f => match sign.(predsymbs) f with
| None => None
| None => Nop
| _ => mo.(preds) f
end).
apply Build_PreModel with fs ps.
......@@ -826,8 +811,7 @@ Proof.
induction t as [ | | f args IH ] using term_ind'; cbn; auto.
destruct (funsymbs sign f); [|easy].
case eqbspec; [|easy]. intros _ F.
destruct (funs mo f) as [(n,ar)|]; auto.
f_equal. apply map_ext_iff. intros t Ht.
f_equiv. apply map_ext_iff. intros t Ht.
apply IH; auto. rewrite forallb_forall in F; auto.
Qed.
......@@ -842,7 +826,6 @@ Proof.
try (rewrite lazy_andb_iff in Hf; destruct Hf); try reflexivity.
- destruct (predsymbs sign p); [|easy].
rewrite lazy_andb_iff in Hf. destruct Hf as (_,Hf).
destruct (preds mo p) as [(n,ar)|]; [|reflexivity].
f_equiv. apply map_ext_iff. intros t Ht.
apply interp_term_restrict. rewrite forallb_forall in Hf; auto.
- now rewrite IHf.
......
(** * N-ary functions *)
(** 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.
(** For function of arity [n], we re-use [NaryFunctions.nfun A n B]
and its notation [A^^n-->B]. *)
(** Then, a compact alternative to [option { n:nat & A^^n-->B }] *)
Inductive optnfun A B :=
| NFun n (f:A^^n-->B)
| Nop.
Arguments Nop {A B}.
Arguments NFun {A B} n f.
Definition get_arity {A B} (f : optnfun A B) :=
match f with
| Nop => None
| NFun n _ => Some n
end.
Fixpoint mk_nprod {A} n (l:list A)(dft:A) : A^n :=
match n, l return A^n with
| 0, _ => tt
| S n, [] => (dft, mk_nprod n l dft)
| S n, x::l => (x, mk_nprod n l dft)
end.
Definition build_args {A B} :=
fix build {n} (l : list A)(dft:B) : A^^n-->B -> B :=
match n, l with
| 0, [] => fun f => f
| S n, a :: l => fun f => build l dft (f a)
| _, _ => fun _ => dft
end.
Definition optnapply {A B}(f:optnfun A B)(l:list A)(dft:B) :=
match f with
| NFun _ f => build_args l dft f
| 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.
Lemma build_map_arity {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).
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 uncurry_curry n (phi : Vector.t A n -> B) v :
uncurry (curry phi) v = phi v.
Proof.
induction v; cbn; auto. now rewrite IHv.
Qed.
Lemma to_vect n (l:list A) :
length l = n -> exists v : Vector.t A n, Vector.to_list v = l.
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.
Qed.
End Curry.
......@@ -4,7 +4,7 @@
(** 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.
Require Import Defs NameProofs Mix Meta Theories Nary PreModels Models.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope string_scope.
......@@ -372,18 +372,18 @@ Qed.
(** A Coq model of this Peano theory, based on the [nat] type *)
Definition PeanoFuns : modfuns nat :=
Definition PeanoFuns : string -> optnfun nat nat :=
fun f =>
if f =? "O" then Some (existT _ 0 0)
else if f =? "S" then Some (existT _ 1 S)
else if f =? "+" then Some (existT _ 2 Nat.add)
else if f =? "*" then Some (existT _ 2 Nat.mul)
else None.
if f =? "O" then NFun 0 0
else if f =? "S" then NFun 1 S
else if f =? "+" then NFun 2 Nat.add
else if f =? "*" then NFun 2 Nat.mul
else Nop.
Definition PeanoPreds : modpreds nat :=
Definition PeanoPreds : string -> optnfun nat Prop :=
fun p =>
if p =? "=" then Some (existT _ 2 (@Logic.eq nat))
else None.
if p =? "=" then NFun 2 Logic.eq
else Nop.
Lemma PeanoFuns_ok s :
funsymbs PeanoSign s = get_arity (PeanoFuns s).
......
......@@ -4,7 +4,7 @@
(** The NatDed development, Pierre Letouzey, 2019.
This file is released under the CC0 License, see the LICENSE file *)
Require Import Defs Mix NameProofs Meta Restrict.
Require Import Defs Mix NameProofs Meta Restrict NaryFunctions Nary.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
......@@ -18,25 +18,12 @@ Set Implicit Arguments.
of the theories, and the facts that their interpretations are
valid. *)
Fixpoint arity_fun A n B :=
match n with
| O => B
| S n => A -> (arity_fun A n B)
end.
Definition get_arity {A B} (o : option { n:nat & arity_fun A n B}) :=
match o with
| None => None
| Some (existT _ n _) => Some n
end.
Definition modfuns M := string -> option { n:nat & arity_fun M n M }.
Definition modpreds M := string -> option { n:nat & arity_fun M n Prop }.
(** TODO: a word why nfun (to use pristine functions like Nat.add in models *)
Record PreModel (M:Type)(sign:signature) :=
{ someone : M; (* M is non-empty *)
funs : modfuns M;
preds : modpreds M;
funs : string -> optnfun M M;
preds : string -> optnfun M Prop;
funsOk : forall s, sign.(funsymbs) s = get_arity (funs s);
predsOk : forall s, sign.(predsymbs) s = get_arity (preds s)
}.
......@@ -54,30 +41,17 @@ Section PREMODEL.
Variable M:Type.
Variable Mo : PreModel M sign.
Definition build_args {A B} :=
fix build n (l : list A)(def:B) : arity_fun A n B -> B :=
match n, l with
| 0, [] => fun f => f
| S n, a :: l => fun f => build n l def (f a)
| _, _ => fun _ => def
end.
(** In case of ill-formed term (w.r.t. signature [sign]), we'll
use the arbitrary point [Mo.(someone)]. Same if we encounter
a local variable larger than the local environment *)
Definition BogusPoint := Mo.(someone).
Definition interp_term genv lenv :=
Definition interp_term G L :=
fix interp t :=
match t with
| FVar x => genv x
| BVar n => nth n lenv BogusPoint
| Fun f args =>
match Mo.(funs) f with
| Some (existT _ n f) =>
build_args n (List.map interp args) BogusPoint f
| None => BogusPoint
end
| FVar x => G x
| BVar n => nth n L BogusPoint
| Fun f args => optnapply (funs Mo f) (List.map interp args) BogusPoint
end.
Definition interp_op o :=
......@@ -91,29 +65,24 @@ Definition interp_op o :=
evaluate to the arbitrary proposition [False]. *)
Definition BogusProp := Logic.False.
Definition interp_form genv :=
fix interp lenv f :=
Definition interp_form G :=
fix interp L f :=
match f with
| True => Logic.True
| False => Logic.False
| Not f => ~(interp lenv f)
| Op o f1 f2 => interp_op o (interp lenv f1) (interp lenv f2)
| Not f => ~(interp L f)
| Op o f1 f2 => interp_op o (interp L f1) (interp L f2)
| Pred p args =>
match Mo.(preds) p with
| Some (existT _ n f) =>
build_args n (List.map (interp_term genv lenv) args) BogusProp f
| None => BogusProp
end
| Quant All f => forall (m:M), interp (m::lenv) f
| Quant Ex f => exists (m:M), interp (m::lenv) f
optnapply (preds Mo p) (List.map (interp_term G L) args) BogusProp
| Quant All f => forall (m:M), interp (m::L) f
| Quant Ex f => exists (m:M), interp (m::L) f
end.
Definition interp_ctx genv lenv l :=
forall f, In f l -> interp_form genv lenv f.
Definition interp_ctx G L l :=
forall f, In f l -> interp_form G L f.
Definition interp_seq genv lenv '(Γ⊢C) :=
interp_ctx genv lenv Γ ->
interp_form genv lenv C.
Definition interp_seq G L '(Γ⊢C) :=
interp_ctx G L Γ -> interp_form G L C.
Lemma interp_term_ext genv genv' lenv t :
(forall v, Names.In v (fvars t) -> genv v = genv' v) ->
......@@ -121,8 +90,7 @@ Lemma interp_term_ext genv genv' lenv t :
Proof.
induction t as [ | |f l IH] using term_ind'; cbn;
intros H; auto with set.
case (Mo.(funs) f) as [(n,fn)|]; cbn; auto. f_equal.
apply map_ext_in. eauto with set.
f_equal. apply map_ext_in. eauto with set.
Qed.
Lemma interp_form_ext genv genv' lenv f :
......@@ -131,9 +99,7 @@ Lemma interp_form_ext genv genv' lenv f :
Proof.
revert lenv.
induction f; cbn; auto; intros; f_equal; auto with set.
- case (Mo.(preds) p) as [(n,fn)|]; cbn; [|reflexivity]; clear p.
f_equiv. clear n fn. apply map_ext_in.
eauto using interp_term_ext with set.
- f_equiv. apply map_ext_in. eauto using interp_term_ext with set.
- rewrite IHf; intuition.
- destruct o; cbn; rewrite IHf1, IHf2; intuition.
- destruct q.
......@@ -165,9 +131,7 @@ Proof.
induction t as [ | |f l IH] using term_ind'; cbn; intros H.
- reflexivity.
- rewrite app_nth1; trivial.
- case (Mo.(funs) f) as [(k,fk)|]; cbn in *; auto. f_equal.
apply map_ext_in.
rewrite list_max_map_le in H. auto.
- f_equiv. apply map_ext_in. rewrite list_max_map_le in H. auto.
Qed.
Lemma interp_term_closed genv lenv t :
......@@ -184,9 +148,7 @@ Lemma interp_form_more_lenv genv lenv lenv' f :
Proof.
revert lenv.
induction f; cbn; intros lenv LE; try tauto.
- case (Mo.(preds) p) as [(k,fk)|]; cbn; [|reflexivity]; clear p.
f_equiv.
apply map_ext_in. intros a Ha.
- f_equiv. apply map_ext_in. intros a Ha.
apply interp_term_more_lenv.
transitivity (list_max (map level l)); auto.
now apply list_max_map_in.
......@@ -214,8 +176,7 @@ Lemma interp_lift genv lenv m t :
interp_term genv (m :: lenv) (lift 0 t) = interp_term genv lenv t.
Proof.
induction t as [ | |f l IH] using term_ind'; cbn; auto.
case (funs Mo f) as [(k,fk)|]; cbn; auto. f_equal.
rewrite map_map. apply map_ext_iff; auto.
f_equiv. rewrite map_map. apply map_ext_iff; auto.
Qed.
Lemma interp_term_bsubst_gen genv lenv lenv' u m n t :
......@@ -230,8 +191,7 @@ Proof.
- case eqbspec; intros; subst; auto.
+ symmetry. now apply nth_error_some_nth.
+ cbn. apply nth_error_ext; auto. symmetry; auto.
- case (Mo.(funs) f) as [(k,fk)|]; cbn; auto. f_equal.
rewrite map_map. apply map_ext_in; auto.
- f_equiv. rewrite map_map. apply map_ext_in; auto.
Qed.
Lemma interp_term_bsubst genv lenv u m n t :
......@@ -261,9 +221,7 @@ Lemma interp_form_bsubst_gen genv lenv lenv' u m n f :
Proof.
revert n u lenv lenv'.
induction f; cbn; auto; intros; f_equal; auto; try reflexivity.
- case (Mo.(preds) p) as [(k,fk)|]; cbn; [|reflexivity]; clear p.
f_equiv.
rewrite map_map. apply map_ext_in. intros a _.
- f_equiv. rewrite map_map. apply map_ext_in. intros a _.
eapply interp_term_bsubst_gen; eauto.
- rewrite (IHf n u lenv lenv'); intuition.
- destruct o; cbn;
......
......@@ -6,8 +6,8 @@
Require Import ChoiceFacts.
Require Vector.
Require Import Defs NameProofs Mix Meta Theories PreModels Models.
Require Import Defs NameProofs Mix Meta.
Require Import Theories NaryFunctions Nary PreModels Models.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope eqb_scope.
......@@ -67,46 +67,6 @@ Proof.
f_equal. rewrite <- seq_shift, map_map. apply IHn. now injection E.
Qed.
(** 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 Notation "A ^ n" := (Vector.t A n) : types_scope.
Local Open Scope types_scope.
Local Open Scope vector_scope.
Fixpoint uncurry {n} : arity_fun A n B -> 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} : (A^n -> B) -> arity_fun 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 uncurry_curry n (phi : A^n -> B) v :
uncurry (curry phi) v = phi v.
Proof.
induction v; cbn; auto. now rewrite IHv.
Qed.
Lemma to_vect n (l:list A) :
length l = n -> exists v : Vector.t A n, Vector.to_list v = l.
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.
Qed.
End Curry.
(** Skolem extension : from a theorem [..∀∃A],
adding a new symbol [f] giving existential witnesses
and the new axiom [xi A(xi,f(xi))].
......@@ -183,10 +143,10 @@ Variable th : theory.
Variable NC : NewCsts th.
Definition Skolem_premodel_ext sign M (mo:PreModel M sign)
f n (phi : arity_fun 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 Some (existT _ n phi) else funs mo s).
set (funs' := fun s => if s =? f then NFun n 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.
......@@ -195,7 +155,7 @@ 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 = None \/ funs mo f = funs mo' f) ->
(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,
......@@ -211,8 +171,7 @@ Proof.
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. destruct (funs mo f) as [(p,q)|]; auto.
unfold BogusPoint. rewrite <- SO. f_equal.
+ rewrite <- Hf. f_equiv; auto.
apply map_ext_in. intros a Ha.
apply IH; auto. rewrite forallb_forall in F; auto. }
induction A; cbn.
......@@ -220,8 +179,7 @@ Proof.
- intuition.
- destruct (predsymbs sign p) as [ar|] eqn:E; try easy.
rewrite lazy_andb_iff. intros (_ & F) genv lenv.
rewrite <- PR. destruct (preds mo p) as [(u,v)|]; try easy.
f_equiv. apply map_ext_in. intros a Ha. apply Ht.
rewrite <- PR. f_equiv. apply map_ext_in. intros a Ha. apply Ht.
rewrite forallb_forall in F; auto.
- intros WA genv l