Commit d1c514c7 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

Mix.bsubst with lift + finished Peano.v (theory and Coq model)

parent 73e3f7d3
......@@ -377,13 +377,16 @@ Proof.
apply Meta.form_level_bsubst_id.
now rewrite nam2mix_level.
+ intros NE.
rewrite lift_nop.
2:{ unfold Mix.BClosed.
generalize (nam2mix_term_level [] u). simpl. omega. }
destruct (Names.mem v (Term.vars u)) eqn:IN; simpl.
* f_equal.
setfresh vars z Hz.
rewrite IH; auto.
f_equal. simpl. apply (nam2mix_rename []); auto with set.
simpl; intuition.
simpl. intros y [<-|Hy]. namedec. auto.
{ f_equal. apply (nam2mix_rename []); auto with set. }
{ simpl; intuition. }
{ simpl. intros y [<-|Hy]. namedec. auto. }
* f_equal. rewrite <- NamesF.not_mem_iff in IN.
apply IH; simpl; intuition; subst; eauto.
Qed.
......
......@@ -8,7 +8,7 @@
# #
###############################################################################
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Meta.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v PreModels.v Models.v parser.v FormulaReader.v
COQMF_VFILES = AsciiOrder.v StringOrder.v StringUtils.v Utils.v Defs.v Nam.v Mix.v NameProofs.v Subst.v Meta.v Equiv.v Equiv2.v AltSubst.v Countable.v Theories.v PreModels.v Models.v Peano.v parser.v FormulaReader.v
COQMF_MLIFILES =
COQMF_MLFILES =
COQMF_ML4FILES =
......
......@@ -10,8 +10,31 @@ Local Open Scope bool_scope.
Local Open Scope lazy_bool_scope.
Local Open Scope eqb_scope.
Implicit Type t u : term.
Implicit Type f : formula.
(** [lift] does nothing on a [BClosed] term *)
Lemma lift_nop t : BClosed t -> lift t = t.
Proof.
unfold BClosed.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
- easy.
- rewrite list_max_map_0. intros H. f_equal. apply map_id_iff; auto.
Qed.
(** [bsubst] and [check] *)
Lemma check_lift sign t :
check sign (lift t) = check sign t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
destruct funsymbs; auto.
rewrite map_length. case eqb; auto.
apply eq_true_iff_eq. rewrite forallb_map, !forallb_forall.
split; intros H x Hx. rewrite <- IH; auto. rewrite IH; auto.
Qed.
Lemma check_bsubst_term sign n (u t:term) :
check sign u = true -> check sign t = true ->
check sign (bsubst n u t) = true.
......@@ -28,18 +51,27 @@ Lemma check_bsubst sign n u (f:formula) :
check sign u = true -> check sign f = true ->
check sign (bsubst n u f) = true.
Proof.
revert n.
induction f; cbn; intros n Hu Hf; auto.
revert n u.
induction f; cbn; intros n u Hu Hf; auto.
- destruct predsymbs; auto.
rewrite !lazy_andb_iff in *. rewrite map_length.
destruct Hf as (Hl,Hl'); split; auto.
rewrite forallb_map, forallb_forall in *.
auto using check_bsubst_term.
- rewrite !lazy_andb_iff in *; intuition.
- apply IHf; auto. now rewrite check_lift.
Qed.
(** [bsubst] and [level] *)
Lemma level_lift t : level (lift t) <= S (level t).
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with arith.
rewrite map_map.
apply list_max_map_le. intros a Ha. transitivity (S (level a)); auto.
rewrite <- Nat.succ_le_mono. now apply list_max_map_in.
Qed.
Lemma level_bsubst_term n (u t:term) :
level t <= S n -> level u <= n ->
level (bsubst n u t) <= n.
......@@ -54,14 +86,43 @@ Lemma level_bsubst n u (f:formula) :
level f <= S n -> level u <= n ->
level (bsubst n u f) <= n.
Proof.
revert n.
induction f; cbn; intros n Hf Hu; auto with arith.
revert n u.
induction f; cbn; intros n u Hf Hu; auto with arith.
- apply (level_bsubst_term n u (Fun "" l)); auto.
- rewrite max_le in *; intuition.
- specialize (IHf (S n)). omega.
- change n with (Nat.pred (S n)) at 2. apply Nat.pred_le_mono.
apply IHf. omega. transitivity (S (level u)). apply level_lift.
omega.
Qed.
Lemma level_bsubst_term' n (u t : term) :
level u <= S n -> level (bsubst n u t) <= level t.
Proof.
intro Hu. revert t. fix IH 1. destruct t; cbn; auto.
- case eqbspec; intros; subst; auto.
- revert l. fix IH' 1. destruct l; cbn; auto.
apply Nat.max_le_compat; auto.
Qed.
(** [bsubst] and [fvars] *)
Lemma level_bsubst' n u (f:formula) :
level u <= S n -> level (bsubst n u f) <= level f.
Proof.
revert n u. induction f; cbn; intros n u Hu; auto with arith.
- now apply (level_bsubst_term' n u (Fun "" l)).
- apply Nat.max_le_compat; auto.
- apply Nat.pred_le_mono; auto with arith.
apply IHf. transitivity (S (level u)). apply level_lift. omega.
Qed.
(** [bsubst] and [fvars] : over-approximations *)
Lemma lift_fvars t : fvars (lift t) = fvars t.
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto with *.
induction l; simpl; auto.
rewrite IH, IHl; simpl; auto.
intros x Hx. apply IH. simpl; auto.
Qed.
Lemma bsubst_term_fvars n (u t:term) :
Names.Subset (fvars (bsubst n u t)) (Names.union (fvars u) (fvars t)).
......@@ -73,10 +134,11 @@ Qed.
Lemma bsubst_fvars n u (f:formula) :
Names.Subset (fvars (bsubst n u f)) (Names.union (fvars u) (fvars f)).
Proof.
revert n.
revert n u.
induction f; cbn; intros; auto with *.
- apply (bsubst_term_fvars n u (Fun "" l)).
- rewrite IHf1, IHf2. namedec.
- rewrite IHf. now rewrite lift_fvars.
Qed.
Lemma bsubst_ctx_fvars n u (c:context) :
......@@ -86,6 +148,29 @@ Proof.
rewrite bsubst_fvars, IH. namedec.
Qed.
(** [bsubst] and [fvars] : under-approximations *)
Lemma bsubst_term_fvars' n (u t : term) :
Names.Subset (fvars t) (fvars (bsubst n u t)).
Proof.
revert t. fix IH 1. destruct t; cbn; auto with set.
clear f.
revert l. fix IH' 1. destruct l; cbn; auto with set.
intro x. NamesF.set_iff. intros [IN|IN].
- left; now apply IH.
- right. now apply IH'.
Qed.
Lemma bsubst_fvars' n u (f:formula) :
Names.Subset (fvars f) (fvars (bsubst n u f)).
Proof.
revert n u; induction f; cbn; intros n u; auto with set.
- apply (bsubst_term_fvars' n u (Fun "" l)).
- intro x. NamesF.set_iff. intros [IN|IN].
left; now apply IHf1.
right; now apply IHf2.
Qed.
(** [bsubst] above the level does nothing *)
Lemma term_level_bsubst_id n u (t:term) :
......@@ -100,8 +185,8 @@ Qed.
Lemma form_level_bsubst_id n u (f:formula) :
level f <= n -> bsubst n u f = f.
Proof.
revert n.
induction f; cbn; intros n LE; f_equal; auto.
revert n u.
induction f; cbn; intros n u LE; f_equal; auto.
- injection (term_level_bsubst_id n u (Fun "" l)); cbn; auto.
- apply IHf1. omega with *.
- apply IHf2. omega with *.
......@@ -114,7 +199,7 @@ Proof.
unfold BClosed. intros. apply term_level_bsubst_id. auto with *.
Qed.
(** [bsubst] to a fesh variable is injective *)
(** [bsubst] to a fresh variable is injective *)
Lemma term_bsubst_fresh_inj n z (t t':term):
~ Names.In z (Names.union (fvars t) (fvars t')) ->
......@@ -313,6 +398,21 @@ Qed.
Definition BClosed_sub (h:variable->term) :=
forall v, BClosed (h v).
Lemma lift_vmap (h:variable->term) t :
lift (vmap h t) = vmap (fun v => lift (h v)) (lift t).
Proof.
induction t as [ | | f l IH] using term_ind'; cbn; auto.
f_equal. rewrite !map_map. apply map_ext_iff; auto.
Qed.
Lemma lift_vmap' (h:variable->term) t :
BClosed_sub h ->
lift (vmap h t) = vmap h (lift t).
Proof.
intros CL. rewrite lift_vmap.
apply term_vmap_ext. intros v _. now apply lift_nop.
Qed.
Lemma term_vmap_bsubst h n u (t:term) :
BClosed_sub h ->
vmap h (bsubst n u t) = bsubst n (vmap h u) (vmap h t).
......@@ -328,9 +428,10 @@ Lemma form_vmap_bsubst h n u (f:formula) :
BClosed_sub h ->
vmap h (bsubst n u f) = bsubst n (vmap h u) (vmap h f).
Proof.
intros CL. revert n.
induction f; cbn; intros n; f_equal; auto.
injection (term_vmap_bsubst h n u (Fun "" l)); auto.
intros CL. revert n u.
induction f; cbn; intros n u; f_equal; auto.
- injection (term_vmap_bsubst h n u (Fun "" l)); auto.
- now rewrite IHf, lift_vmap'.
Qed.
Definition sub_set (x:variable)(t:term)(h:variable->term) :=
......@@ -1249,11 +1350,21 @@ Proof.
f_equal. rewrite !map_map. apply map_ext_iff; auto.
Qed.
Lemma restrict_lift sign x t :
restrict_term sign x (lift t) = lift (restrict_term sign x t).
Proof.
induction t as [ | |f l IH] using term_ind'; cbn; auto.
destruct funsymbs; cbn; auto with *.
rewrite map_length.
case eqbspec; cbn; auto.
intros _. f_equal. rewrite !map_map. apply map_ext_iff; auto.
Qed.
Lemma restrict_bsubst sign x n t f :
restrict sign x (bsubst n t f) =
bsubst n (restrict_term sign x t) (restrict sign x f).
Proof.
revert n.
revert n t.
induction f; cbn; intros; f_equal; auto.
destruct predsymbs; cbn; auto with *.
rewrite map_length.
......@@ -1261,6 +1372,7 @@ Proof.
intros _.
f_equal. rewrite !map_map.
apply map_ext_iff; auto using restrict_term_bsubst.
rewrite <- restrict_lift. auto.
Qed.
Ltac solver :=
......@@ -1620,10 +1732,11 @@ Lemma forcelevel_bsubst n x u f :
forcelevel n x (bsubst n u f) =
bsubst n u (forcelevel (S n) x f).
Proof.
revert n.
revert n u.
induction f; cbn; intros; f_equal; auto.
rewrite !map_map. apply map_ext_iff.
auto using forcelevel_bsubst_term'.
apply IHf. transitivity (S (level u)). apply level_lift. omega.
Qed.
Ltac solver' :=
......
......@@ -219,6 +219,13 @@ Instance term_eqb : Eqb term :=
| _, _ => false
end.
Fixpoint lift t :=
match t with
| BVar n => BVar (S n)
| FVar v => FVar v
| Fun f args => Fun f (List.map lift args)
end.
(** Formulas *)
Inductive formula :=
......@@ -319,13 +326,12 @@ Instance form_level : Level formula :=
| Pred _ args => list_max (map level args)
end.
(** Important note : [bsubst] below is only intended to be
used with a replacement term [t] with no bounded variables !
In a full De Bruijn implementation, we would tweak [t]
(i.e. "lift" it) when entering a quantified part of a formula.
Here it's much simpler to *not* do it, but this may lead to
unexpected results if [t] still has some bounded variables,
see later the treatment of rules ∀e and ∃i. *)
(** Substitution of a bounded variable by a term [t] in a formula [f].
Note : we try to do something sensible when [t] has itself some
bounded variables (we lift them when entering [f]'s quantifiers).
But this situtation is nonetheless to be used with caution.
Actually, we'll almost always use [bsubst] when [t] is [BClosed],
except in [Peano.v]. *)
Instance form_bsubst : BSubst formula :=
fix form_bsubst n t f :=
......@@ -334,7 +340,7 @@ Instance form_bsubst : BSubst formula :=
| Pred p args => Pred p (List.map (bsubst n t) args)
| Not f => Not (form_bsubst n t f)
| Op o f f' => Op o (form_bsubst n t f) (form_bsubst n t f')
| Quant q f' => Quant q (form_bsubst (S n) t f')
| Quant q f' => Quant q (form_bsubst (S n) (lift t) f')
end.
Instance form_fvars : FVars formula :=
......
......@@ -656,7 +656,7 @@ Fixpoint height f :=
Lemma height_bsubst n t f :
height (bsubst n t f) = height f.
Proof.
revert n.
revert n t.
induction f; cbn; f_equal; auto.
Qed.
......
Require Import Defs NameProofs Mix Theories Meta.
(** * The Theory of Peano Arithmetic and its Coq model *)
(** 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.
Import ListNotations.
Local Open Scope bool_scope.
Local Open Scope eqb_scope.
(** The Peano axioms *)
Definition PeanoSign := Finite.to_infinite peano_sign.
Definition Zero := Fun "O" [].
Definition Succ x := Fun "S" [x].
......@@ -26,7 +35,7 @@ Definition ax8 := ∀∀∀ (#1 = #0 -> #2 * #1 = #2 * #0).
Definition ax9 := (Zero + #0 = #0).
Definition ax10 := ∀∀ (Succ(#1) + #0 = Succ(#1 + #0)).
Definition ax11 := (Zero * #0 = #0).
Definition ax11 := (Zero * #0 = Zero).
Definition ax12 := ∀∀ (Succ(#1) * #0 = (#1 * #0) + #0).
Definition ax13 := ∀∀ (Succ(#1) = Succ(#0) -> #1 = #0).
......@@ -36,152 +45,28 @@ Definition axioms_list :=
[ ax1; ax2; ax3; ax4; ax5; ax6; ax7; ax8;
ax9; ax10; ax11; ax12; ax13; ax14 ].
Fixpoint nForall n A :=
match n with
| 0 => A
| S n => ( (nForall n A))%form
end.
Lemma nForall_check sign n A :
check sign (nForall n A) = check sign A.
Proof.
induction n; simpl; auto.
Qed.
Lemma nForall_fclosed n A :
FClosed A -> FClosed (nForall n A).
Proof.
induction n; simpl; auto.
Qed.
Lemma nForall_level n A :
level (nForall n A) = level A - n.
Proof.
induction n; cbn; auto with arith.
rewrite IHn. omega.
Qed.
(** Change all bound vars [#n] into [h #n], with lifting
under quantifiers *)
Fixpoint form_update n (h:term->term) f :=
match f with
| True | False => f
| Pred p args => Pred p (List.map (bsubst n (h (BVar n))) args)
| Not f => Not (form_update n h f)
| Op o f f' => Op o (form_update n h f) (form_update n h f')
| Quant q f' => Quant q (form_update (S n) h f')
end.
Lemma form_update_check sign (h:term->term) :
(forall n, check sign (h (BVar n)) = true) ->
forall f n, check sign f = true ->
check sign (form_update n h f) = true.
Proof.
intros Hh. induction f; cbn; intros n; auto.
- destruct predsymbs; auto.
rewrite !lazy_andb_iff.
rewrite map_length. intuition.
rewrite forallb_forall in *. intros t Ht.
rewrite in_map_iff in Ht. destruct Ht as (t' & <- & IN).
apply check_bsubst_term; auto.
- rewrite !lazy_andb_iff; intuition.
Qed.
Lemma bsubst_term_fvars' n (u t : term) :
Names.Subset (fvars t) (fvars (bsubst n u t)).
Proof.
revert t. fix IH 1. destruct t; cbn; auto with set.
clear f.
revert l. fix IH' 1. destruct l; cbn; auto with set.
intro x. NamesF.set_iff. intros [IN|IN].
- left; now apply IH.
- right. now apply IH'.
Qed.
Lemma bsubst_fvars' n u (f:formula) :
Names.Subset (fvars f) (fvars (bsubst n u f)).
Proof.
revert n; induction f; cbn; intros n; auto with set.
- apply (bsubst_term_fvars' n u (Fun "" l)).
- intro x. NamesF.set_iff. intros [IN|IN].
left; now apply IHf1.
right; now apply IHf2.
Qed.
Lemma form_update_fvars (h:term->term) :
(forall n, FClosed (h (BVar n))) ->
forall f n, Names.Equal (fvars (form_update n h f)) (fvars f).
Proof.
intros Hh. induction f; cbn; intros n; auto with set.
- intro x. rewrite unionmap_map_in, unionmap_in.
split.
+ intros (a & IN & IN'). exists a; split; auto.
apply bsubst_term_fvars in IN.
rewrite Names.union_spec in IN. destruct IN; auto.
now apply Hh in H.
+ intros (a & IN & IN'). exists a; split; auto.
now apply bsubst_term_fvars'.
- intros x. NamesF.set_iff. now rewrite IHf1, IHf2.
Qed.
Lemma form_update_closed (h:term->term) :
(forall n, FClosed (h (BVar n))) ->
forall f n, FClosed f -> FClosed (form_update n h f).
Proof.
intros. red. rewrite form_update_fvars; auto.
Qed.
Lemma level_bsubst_term' n (u t : term) :
level u <= S n -> level (bsubst n u t) <= level t.
Proof.
intro Hu. revert t. fix IH 1. destruct t; cbn; auto.
- case eqbspec; intros; subst; auto.
- revert l. fix IH' 1. destruct l; cbn; auto.
apply Nat.max_le_compat; auto.
Qed.
Lemma level_bsubst' n u (f:formula) :
level u <= S n -> level (bsubst n u f) <= level f.
Proof.
revert n. induction f; cbn; intros n Hu; auto with arith.
- now apply (level_bsubst_term' n u (Fun "" l)).
- apply Nat.max_le_compat; auto.
- apply Nat.pred_le_mono; auto with arith.
Qed.
Lemma form_update_level (h:term->term) :
(forall n, level (h (BVar n)) <= S n) ->
forall f n, level (form_update n h f) <= level f.
Proof.
intros Hh. induction f; cbn; intros n; auto.
- apply (level_bsubst_term' n (h (#n)) (Fun "" l)); auto.
- apply Nat.max_le_compat; auto.
- apply Nat.pred_le_mono; auto.
Qed.
(** Beware, bsubst would not be ok below for turning [#0] into [Succ #0]
(no lift on substituted term inside quantifiers).
(** Beware, [bsubst] is ok below for turning [#0] into [Succ #0], but
only since it contains now a [lift] of substituted terms inside
quantifiers.
And the unconventional [] before [A[0]] is to get the right
bounded vars (Hack !). *)
Definition induction_schema A :=
let n := level A in
Definition induction_schema A_x :=
let A_0 := bsubst 0 Zero A_x in
let A_Sx := bsubst 0 (Succ(#0)) A_x in
nForall
(pred n)
( (bsubst 0 Zero A) /\ ( (A -> form_update 0 Succ A)) -> A).
(Nat.pred (level A_x))
((( A_0) /\ ( (A_x -> A_Sx))) -> A_x).
Local Close Scope formula_scope.
Definition peano_sign' := Finite.to_infinite peano_sign.
Definition IsAx A :=
List.In A axioms_list \/
exists B, A = induction_schema B /\
check peano_sign' B = true /\
check PeanoSign B = true /\
FClosed B.
Lemma WfAx A : IsAx A -> Wf peano_sign' A.
Lemma WfAx A : IsAx A -> Wf PeanoSign A.
Proof.
intros [ IN | (B & -> & HB & HB')].
- apply Wf_iff.
......@@ -189,27 +74,94 @@ Proof.
simpl in IN. intuition; subst; reflexivity.
- repeat split; unfold induction_schema; cbn.
+ rewrite nForall_check. cbn.
rewrite check_bsubst, HB; auto.
rewrite form_update_check; auto.
rewrite !check_bsubst, HB; auto.
+ red. rewrite nForall_level. cbn.
assert (level (bsubst 0 Zero B) <= level B).
{ apply level_bsubst'. auto. }
assert (level (form_update 0 Succ B) <= level B).
{ apply form_update_level. auto. }
assert (level (bsubst 0 (Succ(BVar 0)) B) <= level B).
{ apply level_bsubst'. auto. }
omega with *.
+ apply nForall_fclosed. red. cbn.
rewrite form_update_fvars; auto.
assert (FClosed (bsubst 0 Zero B)).
{ red. rewrite bsubst_fvars.
intro x. rewrite Names.union_spec. cbn. red in HB'. intuition. }
assert (FClosed (bsubst 0 (Succ(BVar 0)) B)).
{ red. rewrite bsubst_fvars.
intro x. rewrite Names.union_spec. cbn - [Names.union].
rewrite Names.union_spec.
generalize (HB' x) (@Names.empty_spec x). intuition. }
unfold FClosed in *. intuition.
Qed.
End PeanoAx.
Local Open Scope string.
Definition PeanoTheory :=
{| sign := Finite.to_infinite peano_sign;
{| sign := PeanoSign;
IsAxiom := PeanoAx.IsAx;
WfAxiom := PeanoAx.WfAx |}.
(** TODO : modele *)
(** A Coq model of this Peano theory, based on the [nat] type *)
Definition PeanoFuns : modfuns 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.
Definition PeanoPreds : modpreds nat :=
fun p =>
if p =? "=" then Some (existT _ 2 (@Logic.eq nat))
else None.
Lemma PeanoFuns_ok s :
funsymbs PeanoSign s = get_arity (PeanoFuns s).
Proof.
unfold PeanoSign, peano_sign, PeanoFuns. simpl.
unfold eqb, eqb_inst_string.
repeat (case string_eqb; auto).
Qed.
Lemma PeanoPreds_ok s :
predsymbs PeanoSign s = get_arity (PeanoPreds s).
Proof.
unfold PeanoSign, peano_sign, PeanoPreds. simpl.
unfold eqb, eqb_inst_string.
case string_eqb; auto.
Qed.
Definition PeanoPreModel : PreModel nat PeanoTheory :=
{| someone := 0;
funs := PeanoFuns;
preds := PeanoPreds;
funsOk := PeanoFuns_ok;
predsOk := PeanoPreds_ok |}.