Models.v reworked, lighter use of dependent types

Defs.v

@@ -171,12 +171,15 @@ Qed.
 
 (** Which logic are we using : classical or intuitionistic ? *)
 
-Inductive logic := Classic | Intuiti.
+Inductive logic := K | J.
+
+Definition Classic := K.
+Definition Intuiti := J.
 
 Instance logic_eqb : Eqb logic :=
   fun l1 l2 =>
     match l1, l2 with
-    | Classic, Classic | Intuiti, Intuiti => true
+    | K, K | J, J => true
     | _, _ => false
     end.
 

Nary.v

@@ -10,60 +10,17 @@ 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.
-
-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}.
+Arguments nfun_to_nfun {A B C} f {n}.
 
-Lemma build_args_ntn {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' (nfun_to_nfun f a) = f (build_args l any a).
-Proof.
- intros <-. induction l; simpl; auto.
-Qed.
-
-Lemma to_nprod {A} n (l:list A) :
-  length l = n -> exists v : A^n, nprod_to_list v = l.
+Lemma nuncurry_ncurry {A B n} (f : A^n->B) (v:A^n) :
+  nuncurry (ncurry f) v = f v.
 Proof.
- intros <-.
- exists (nprod_of_list _ l). induction l; cbn; f_equal; auto.
+ induction n; cbn in *; auto.
+ - now destruct v.
+ - destruct v as (a,v). now rewrite IHn.
 Qed.
 
 Lemma nprod_to_list_length {A} n (v:A^n) :
@@ -72,17 +29,73 @@ Proof.
  induction n; cbn; auto. destruct v; cbn; auto.
 Qed.
 
-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.
+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) :=
+ match n, l return option (A^n) with
+ | 0, []  => Some tt
+ | S n, x::l => option_map (pair x) (optnprod n l)
+ | _, _ => None
+ end.
+
+Lemma optnprod_some {A} n (l:list A) :
+  optnprod n l <> None <-> length l = n.
 Proof.
- induction n; cbn in *; auto.
- destruct v as (a,v). apply IHn.
+ revert l. induction n; destruct l; cbn; try easy.
+ specialize (IHn l).
+ destruct (optnprod n l); cbn in *; intuition; try easy.
+ f_equal. now apply H.
 Qed.
 
-Lemma nuncurry_ncurry {A B n} (f : A^n->B) (v:A^n) :
-  nuncurry (ncurry f) v = f v.
+Lemma optnprod_to_list {A} n (l:list A) (v:A^n) :
+ optnprod n l = Some v <-> nprod_to_list v = l.
 Proof.
- induction n; cbn in *; auto.
+ revert l. induction n; destruct l; cbn in *.
  - now destruct v.
- - destruct v as (a,v). now rewrite IHn.
+ - now intuition.
+ - now intuition.
+ - destruct v as (b,v). specialize (IHn v l).
+   destruct (optnprod n l); cbn.
+   + split; intros [= <- <-]; f_equal. now apply IHn.
+     intuition. congruence.
+   + split. easy. intros [= <- <-]. now intuition.
 Qed.
+
+(** 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.
+
+Definition optnapply {A B}(f:optnfun A B)(l:list A) :=
+ match f with
+ | NFun n f => option_map (nuncurry f) (optnprod n l)
+ | Nop => None
+ end.
+
+Definition napply_dft {A B}(f:optnfun A B)(l:list A)(dft:B) :=
+ match optnapply f l with
+ | Some b => b
+ | None => dft
+ end.

PreModels.v

@@ -14,11 +14,25 @@ Set Implicit Arguments.
 
 (** A pre-model (also called a Σ-structure) is a non-empty domain M
     alongside some interpretations for function symbols and predicate
-    symbols. For a full model of a theorie, we'll need the axioms
-    of the theories, and the facts that their interpretations are
-    valid. *)
-
-(** TODO: a word why nfun (to use pristine functions like Nat.add in models *)
+    symbols. For a full model of a theory, we'll need later to ensure
+    that all axioms of this theory have valid interpretations, see
+    [Models.v].
+
+    For encoding the interpretations of symbols, we use [Nary.optnfun],
+    which is based on [NaryFunctions.nfun], the dependent type of
+    functions of arity [n]. More precisely, an [optnfun] is either
+    [Nop] for symbols not in the signature, or [NFun n f], where
+    [f] is a function expecting [n] arguments. Note that [n] is
+    internal (existential), and may be retrieved via [get_arity].
+
+    This choice of representation allows the direct use of Coq
+    usual functions in concrete models, e.g. [NFun 2 Nat.add] for
+    Peano's "+". But [nfun] may be tricky to use in proofs,
+    so we often switch to an equivalent forms based
+    on dependent n-uplets [NaryFunctions.nprod], thanks to
+    [NaryFunctions.nuncurry] and [NaryFunctions.ncurry]. These
+    n-uplets are iterated pairs, but Coq Vectors could also have
+    been considered. *)
 
 Record PreModel (M:Type)(sign:signature) :=
   { someone : M; (* M is non-empty *)
@@ -29,7 +43,7 @@ Record PreModel (M:Type)(sign:signature) :=
   }.
 
 (** Note: actually, we're not using [sign], [funsOk], [predsOK]
-    anywhere in this file !! See [BogusPoint] below :
+    anywhere in this part !! See [BogusPoint] below :
     if an interpretation hasn't the right arity, we'll proceed
     nonetheless, ending up with dummy formulas that won't allow
     later to prove that the axioms of our theory are valid in
@@ -51,7 +65,7 @@ Definition interp_term G L :=
     match t with
     | FVar x => G x
     | BVar n => nth n L BogusPoint
-    | Fun f args => optnapply (funs Mo f) (List.map interp args) BogusPoint
+    | Fun f args => napply_dft (funs Mo f) (List.map interp args) BogusPoint
     end.
 
 Definition interp_op o :=
@@ -73,7 +87,7 @@ Definition interp_form G :=
     | Not f => ~(interp L f)
     | Op o f1 f2 => interp_op o (interp L f1) (interp L f2)
     | Pred p args =>
-      optnapply (preds Mo p) (List.map (interp_term G L) args) BogusProp
+      napply_dft (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.
@@ -294,8 +308,8 @@ Hint Resolve interp_ctx_cons.
 
 Definition CoqRequirements lg :=
  match lg with
- | Classic => forall A:Prop, A\/~A
- | Intuiti => Logic.True
+ | K => forall A:Prop, A\/~A
+ | J => Logic.True
  end.
 
 (** Note: we do not ask here for the derivation [d] to be

Skolem.v

@@ -230,19 +230,20 @@ intros A0 [ | -> ] genv.
   rewrite interp_nforall. intros. rewrite app_nil_r.
   destruct stk as [|m l]; try easy.
   injection H as H.
-  rewrite <- rev_length in H.
-  destruct (to_nprod _ _ H) as (v & Hv).
+  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.
   + unfold th'. simpl.
     rewrite <- (interp_form_skolem_premodel_ext th M f n Phi mo); auto.
-    * rewrite <- (rev_involutive l), <- Hv. apply Hphi.
+    * apply optnprod_to_list in Ev.
+      rewrite <- (rev_involutive l), <- Ev. apply Hphi.
     * clear -Thm. destruct Thm as (((CA,_),_),_).
       rewrite nForall_check in CA. apply CA.
   + simpl nth_error. f_equal.
     cbn. rewrite eqb_refl.
-    rewrite interp_downvars, <- Hv by (now rewrite rev_length in H).
-    symmetry. clear -v. unfold Phi.
-    rewrite <- (nuncurry_ncurry phi v). cbn. apply build_args_nprod.
+    rewrite interp_downvars; auto.
+    unfold Phi. unfold napply_dft. cbn.
+    rewrite Ev. cbn. now rewrite nuncurry_ncurry.
   + destruct k; try easy.
 Qed.
 

Utils.v

@@ -30,6 +30,11 @@ Proof.
  reflexivity.
 Qed.
 
+Lemma option_nat_dec (o o' : option nat) : { o = o' }+{ o <> o' }.
+Proof.
+ decide equality. apply Nat.eq_dec.
+Defined.
+
 (** Generic boolean equalities (via Coq Classes) *)
 
 Delimit Scope eqb_scope with eqb.
@@ -414,6 +419,14 @@ Proof.
  apply max_mono; auto.
 Qed.
 
+Lemma list_max_map_ext {A} (f g : A->nat) l :
+ (forall a, In a l -> f a = g a) ->
+ list_max (map f l) = list_max (map g l).
+Proof.
+ intros H.
+ induction l; cbn in *; auto.
+Qed.
+
 Lemma list_max_in l a : In a l -> a <= list_max l.
 Proof.
  induction l; simpl.
@@ -457,6 +470,13 @@ Proof.
  induction l; simpl; f_equal; auto.
 Qed.
 
+Lemma forallb_ext {A} (f f':A->bool) l :
+  (forall a, In a l -> f a = f' a) -> forallb f l = forallb f' l.
+Proof.
+ induction l; intros E; cbn in *; auto. rewrite <- E by now left.
+ f_equal. apply IHl. intros a' Ha'. apply E. now right.
+Qed.
+
 (** Nth *)
 
 Lemma nth_error_some_nth {A} (l:list A) n a d :