Peano.v 12.3 KB
 Pierre Letouzey committed Jul 10, 2019 1 `````` `````` Pierre Letouzey committed Aug 09, 2019 2 3 4 5 6 7 ``````(** * 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. `````` Pierre Letouzey committed Jul 10, 2019 8 9 10 11 ``````Import ListNotations. Local Open Scope bool_scope. Local Open Scope eqb_scope. `````` Pierre Letouzey committed Aug 09, 2019 12 13 14 15 ``````(** The Peano axioms *) Definition PeanoSign := Finite.to_infinite peano_sign. `````` Samuel Ben Hamou committed Jul 07, 2020 16 17 ``````Notation Zero := (Fun "O" []). Notation Succ x := (Fun "S" [x]). `````` Pierre Letouzey committed Jul 10, 2019 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 `````` Notation "x = y" := (Pred "=" [x;y]) : formula_scope. Notation "x + y" := (Fun "+" [x;y]) : formula_scope. Notation "x * y" := (Fun "*" [x;y]) : formula_scope. Module PeanoAx. Local Open Scope formula_scope. Definition ax1 := ∀ (#0 = #0). Definition ax2 := ∀∀ (#1 = #0 -> #0 = #1). Definition ax3 := ∀∀∀ (#2 = #1 /\ #1 = #0 -> #2 = #0). Definition ax4 := ∀∀ (#1 = #0 -> Succ (#1) = Succ (#0)). Definition ax5 := ∀∀∀ (#2 = #1 -> #2 + #0 = #1 + #0). Definition ax6 := ∀∀∀ (#1 = #0 -> #2 + #1 = #2 + #0). Definition ax7 := ∀∀∀ (#2 = #1 -> #2 * #0 = #1 * #0). Definition ax8 := ∀∀∀ (#1 = #0 -> #2 * #1 = #2 * #0). Definition ax9 := ∀ (Zero + #0 = #0). Definition ax10 := ∀∀ (Succ(#1) + #0 = Succ(#1 + #0)). `````` Pierre Letouzey committed Aug 09, 2019 38 ``````Definition ax11 := ∀ (Zero * #0 = Zero). `````` Pierre Letouzey committed Jul 10, 2019 39 40 41 42 43 44 ``````Definition ax12 := ∀∀ (Succ(#1) * #0 = (#1 * #0) + #0). Definition ax13 := ∀∀ (Succ(#1) = Succ(#0) -> #1 = #0). Definition ax14 := ∀ ~(Succ(#0) = Zero). Definition axioms_list := `````` 45 `````` [ ax1; ax2; ax3; ax4; ax5; ax6; ax7; ax8; `````` Pierre Letouzey committed Jul 10, 2019 46 47 `````` ax9; ax10; ax11; ax12; ax13; ax14 ]. `````` Pierre Letouzey committed Aug 09, 2019 48 49 50 ``````(** Beware, [bsubst] is ok below for turning [#0] into [Succ #0], but only since it contains now a [lift] of substituted terms inside quantifiers. `````` Pierre Letouzey committed Jul 10, 2019 51 52 53 `````` And the unconventional [∀] before [A[0]] is to get the right bounded vars (Hack !). *) `````` Pierre Letouzey committed Aug 09, 2019 54 55 56 ``````Definition induction_schema A_x := let A_0 := bsubst 0 Zero A_x in let A_Sx := bsubst 0 (Succ(#0)) A_x in `````` Pierre Letouzey committed Jul 10, 2019 57 `````` nForall `````` Pierre Letouzey committed Aug 09, 2019 58 59 `````` (Nat.pred (level A_x)) (((∀ A_0) /\ (∀ (A_x -> A_Sx))) -> ∀ A_x). `````` Pierre Letouzey committed Jul 10, 2019 60 61 62 63 64 65 `````` Local Close Scope formula_scope. Definition IsAx A := List.In A axioms_list \/ exists B, A = induction_schema B /\ `````` Pierre Letouzey committed Aug 09, 2019 66 `````` check PeanoSign B = true /\ `````` Pierre Letouzey committed Jul 10, 2019 67 68 `````` FClosed B. `````` Pierre Letouzey committed Aug 09, 2019 69 ``````Lemma WfAx A : IsAx A -> Wf PeanoSign A. `````` Pierre Letouzey committed Jul 10, 2019 70 71 72 73 74 75 76 ``````Proof. intros [ IN | (B & -> & HB & HB')]. - apply Wf_iff. unfold axioms_list in IN. simpl in IN. intuition; subst; reflexivity. - repeat split; unfold induction_schema; cbn. + rewrite nForall_check. cbn. `````` Pierre Letouzey committed Aug 09, 2019 77 `````` rewrite !check_bsubst, HB; auto. `````` Pierre Letouzey committed Jul 10, 2019 78 79 80 `````` + red. rewrite nForall_level. cbn. assert (level (bsubst 0 Zero B) <= level B). { apply level_bsubst'. auto. } `````` Pierre Letouzey committed Aug 09, 2019 81 82 `````` assert (level (bsubst 0 (Succ(BVar 0)) B) <= level B). { apply level_bsubst'. auto. } `````` Pierre Letouzey committed Jul 10, 2019 83 `````` omega with *. `````` 84 85 `````` + apply nForall_fclosed. rewrite <- form_fclosed_spec in *. cbn. now rewrite !fclosed_bsubst, HB'. `````` Pierre Letouzey committed Jul 10, 2019 86 87 88 89 ``````Qed. End PeanoAx. `````` Pierre Letouzey committed Aug 09, 2019 90 ``````Local Open Scope string. `````` 91 92 ``````Local Open Scope formula_scope. `````` Pierre Letouzey committed Jul 10, 2019 93 ``````Definition PeanoTheory := `````` Pierre Letouzey committed Aug 09, 2019 94 `````` {| sign := PeanoSign; `````` Pierre Letouzey committed Jul 10, 2019 95 96 97 `````` IsAxiom := PeanoAx.IsAx; WfAxiom := PeanoAx.WfAx |}. `````` 98 ``````(** Useful lemmas so as to be able to write proofs that take less than 1000 lines. *) `````` Samuel Ben Hamou committed Jun 08, 2020 99 `````` `````` 100 101 ``````Import PeanoAx. `````` Pierre Letouzey committed Jul 10, 2020 102 ``````Lemma Symmetry : forall logic A B Γ, BClosed A -> In ax2 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ B = A). `````` 103 104 105 106 ``````Proof. intros. apply R_Imp_e with (A := A = B); [ | assumption ]. assert (AX2 : Pr logic (Γ ⊢ ax2)). `````` Pierre Letouzey committed Jul 10, 2020 107 `````` { apply R_Ax. exact H0. } `````` 108 `````` unfold ax2 in AX2. `````` Pierre Letouzey committed Jul 10, 2020 109 110 `````` apply R_All_e with (t := A) in AX2. apply R_All_e with (t := B) in AX2. `````` 111 112 `````` cbn in AX2. assert (bsubst 0 B (lift A) = A). `````` Pierre Letouzey committed Jul 10, 2020 113 114 `````` { assert (lift A = A). { apply lift_nop. exact H. } rewrite H2. apply bclosed_bsubst_id. exact H. } rewrite H2 in AX2. `````` 115 116 117 `````` exact AX2. Qed. `````` Pierre Letouzey committed Jul 10, 2020 118 ``````Lemma Transitivity : forall logic A B C Γ, BClosed A -> BClosed B -> In ax3 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ B = C) -> Pr logic (Γ ⊢ A = C). `````` 119 120 121 122 ``````Proof. intros. apply R_Imp_e with (A := A = B /\ B = C); [ | apply R_And_i; assumption ]. assert (AX3 : Pr logic (Γ ⊢ ax3)). `````` Pierre Letouzey committed Jul 10, 2020 123 `````` { apply R_Ax. exact H1. } `````` 124 `````` unfold ax3 in AX3. `````` Pierre Letouzey committed Jul 10, 2020 125 126 127 `````` apply R_All_e with (t := A) in AX3. apply R_All_e with (t := B) in AX3. apply R_All_e with (t := C) in AX3. `````` 128 129 `````` cbn in AX3. assert (bsubst 0 C (lift B) = B). `````` Pierre Letouzey committed Jul 10, 2020 130 131 `````` { assert (lift B = B). {apply lift_nop. assumption. } rewrite H4. apply bclosed_bsubst_id. assumption. } rewrite H4 in AX3. `````` 132 `````` assert (bsubst 0 C (bsubst 1 (lift B) (lift (lift A))) = A). `````` Pierre Letouzey committed Jul 10, 2020 133 134 135 `````` { assert (lift A = A). { apply lift_nop. assumption. } rewrite H5. rewrite H5. assert (lift B = B). { apply lift_nop. assumption. } rewrite H6. assert (bsubst 1 B A = A). { apply bclosed_bsubst_id. assumption. } rewrite H7. `````` 136 `````` apply bclosed_bsubst_id. assumption. } `````` Pierre Letouzey committed Jul 10, 2020 137 `````` rewrite H5 in AX3. `````` 138 139 140 `````` assumption. Qed. `````` Pierre Letouzey committed Jul 10, 2020 141 ``````Lemma Hereditarity : forall logic A B Γ, BClosed A -> In ax4 Γ -> Pr logic (Γ ⊢ A = B) -> Pr logic (Γ ⊢ Succ A = Succ B). `````` 142 143 144 145 146 147 ``````Proof. intros. apply R_Imp_e with (A := A = B); [ | assumption ]. assert (AX4 : Pr logic (Γ ⊢ ax4)). { apply R_Ax. assumption. } unfold ax4 in AX4. `````` Pierre Letouzey committed Jul 10, 2020 148 149 `````` apply R_All_e with (t := A) in AX4. apply R_All_e with (t := B) in AX4. `````` 150 151 `````` cbn in AX4. assert (bsubst 0 B (lift A) = A). `````` Pierre Letouzey committed Jul 10, 2020 152 `````` { assert (lift A = A). { apply lift_nop. assumption. } rewrite H2. `````` 153 `````` apply bclosed_bsubst_id. assumption. } `````` Pierre Letouzey committed Jul 10, 2020 154 `````` rewrite H2 in AX4. `````` 155 156 157 `````` assumption. Qed. `````` Pierre Letouzey committed Jul 10, 2020 158 ``````Lemma AntiHereditarity : forall logic A B Γ, BClosed A -> In ax13 Γ -> Pr logic (Γ ⊢ Succ A = Succ B) -> Pr logic (Γ ⊢ A = B). `````` 159 160 161 162 163 164 ``````Proof. intros. apply R_Imp_e with (A := Succ A = Succ B); [ | assumption ]. assert (AX13 : Pr logic (Γ ⊢ ax13)). { apply R_Ax. assumption. } unfold ax13 in AX13. `````` Pierre Letouzey committed Jul 10, 2020 165 166 `````` apply R_All_e with (t := A) in AX13. apply R_All_e with (t := B) in AX13. `````` 167 168 `````` cbn in AX13. assert (bsubst 0 B (lift A) = A). `````` Pierre Letouzey committed Jul 10, 2020 169 `````` { assert (lift A = A). { apply lift_nop. assumption. } rewrite H2. `````` 170 `````` apply bclosed_bsubst_id. assumption. } `````` Pierre Letouzey committed Jul 10, 2020 171 `````` rewrite H2 in AX13. `````` 172 173 174 `````` assumption. Qed. `````` Samuel Ben Hamou committed Jul 07, 2020 175 176 177 178 179 180 181 182 183 184 185 186 187 ``````Lemma IsAx_adhoc form : check PeanoSign form = true -> FClosed form -> Forall IsAx (induction_schema form ::axioms_list). Proof. intros. apply Forall_forall. intros x Hx. destruct Hx. + simpl. unfold IsAx. right. exists form. split; [ auto | split; [ auto | auto ]]. + simpl. unfold IsAx. left. assumption. Qed. `````` Samuel Ben Hamou committed Jul 08, 2020 188 ``````Lemma rec0_rule l Γ A_x : `````` Samuel Ben Hamou committed Jul 07, 2020 189 `````` BClosed (∀ A_x) -> `````` Samuel Ben Hamou committed Jul 08, 2020 190 191 192 193 `````` In (induction_schema A_x) Γ -> Pr l (Γ ⊢ bsubst 0 Zero A_x) -> Pr l (Γ ⊢ ∀ (A_x -> bsubst 0 (Succ(#0)) A_x)) -> Pr l (Γ ⊢ ∀ A_x). `````` Samuel Ben Hamou committed Jul 07, 2020 194 195 196 197 198 199 200 201 202 203 204 205 ``````Proof. intros. eapply R_Imp_e. + apply R_Ax. unfold induction_schema in H0. unfold BClosed in H. cbn in H. rewrite H in H0. cbn in H0. apply H0. + simpl. apply R_And_i; cbn. `````` Samuel Ben Hamou committed Jul 08, 2020 206 `````` * set (v := fresh (fvars (Γ ⊢ ∀ bsubst 0 Zero A_x)%form)). `````` Samuel Ben Hamou committed Jul 07, 2020 207 208 209 210 211 212 213 214 215 216 217 218 `````` apply R_All_i with (x:=v). apply fresh_ok. rewrite form_level_bsubst_id. - assumption. - apply level_bsubst. ++ unfold BClosed in H. cbn in H; omega. ++ cbn; omega. * assumption. Qed. (* And tactics to make the proofs look like natural deduction proofs. *) `````` Samuel Ben Hamou committed Jul 21, 2020 219 220 221 222 223 224 225 ``````Ltac reIff := match goal with | |- context [ ((?A -> ?B) /\ _ )%form ] => fold (Iff A B); reIff | H : context [ ((?A -> ?B) /\ _ )%form ] |- _ => fold (Iff A B) in H; reIff | _ => idtac end. `````` Samuel Ben Hamou committed Jul 07, 2020 226 ``````Ltac calc := `````` Samuel Ben Hamou committed Jun 16, 2020 227 `````` match goal with `````` Samuel Ben Hamou committed Jul 07, 2020 228 229 230 231 `````` | |- BClosed _ => reflexivity | |- In _ _ => rewrite <- list_mem_in; reflexivity | |- ~Names.In _ _ => rewrite<- Names.mem_spec; now compute | _ => idtac `````` Samuel Ben Hamou committed Jun 16, 2020 232 `````` end. `````` Samuel Ben Hamou committed Jun 12, 2020 233 `````` `````` Samuel Ben Hamou committed Jul 07, 2020 234 235 236 ``````Ltac inst H l := match l with | [] => idtac `````` Pierre Letouzey committed Jul 10, 2020 237 `````` | (?u::?l) => apply R_All_e with (t := u) in H; inst H l `````` Samuel Ben Hamou committed Jul 07, 2020 238 `````` end. `````` Samuel Ben Hamou committed Jun 12, 2020 239 `````` `````` Samuel Ben Hamou committed Jul 07, 2020 240 241 242 243 ``````Ltac axiom ax name := match goal with | |- Pr ?l (?ctx ⊢ _) => assert (name : Pr l (ctx ⊢ ax)); [ apply R_Ax; calc | ]; unfold ax in name end. `````` Samuel Ben Hamou committed Jun 12, 2020 244 `````` `````` Samuel Ben Hamou committed Jul 07, 2020 245 246 ``````Ltac inst_axiom ax l := let H := fresh in `````` Samuel Ben Hamou committed Jul 17, 2020 247 `````` axiom ax H; inst H l; try easy. `````` Samuel Ben Hamou committed Jun 12, 2020 248 `````` `````` Samuel Ben Hamou committed Jul 21, 2020 249 ``````Ltac app_R_All_i t v := apply R_All_i with (x := t); calc; cbn; set (v := FVar t); reIff. `````` Samuel Ben Hamou committed Jul 07, 2020 250 ``````Ltac eapp_R_All_i := eapply R_All_i; calc. `````` Samuel Ben Hamou committed Jun 12, 2020 251 `````` `````` Samuel Ben Hamou committed Jul 07, 2020 252 ``````Ltac sym := apply Symmetry; calc. `````` Samuel Ben Hamou committed Jun 12, 2020 253 `````` `````` Samuel Ben Hamou committed Jul 07, 2020 254 ``````Ltac ahered := apply Hereditarity; calc. `````` Samuel Ben Hamou committed Jun 12, 2020 255 `````` `````` Samuel Ben Hamou committed Jul 07, 2020 256 ``````Ltac hered := apply AntiHereditarity; calc. `````` Samuel Ben Hamou committed Jun 16, 2020 257 `````` `````` Samuel Ben Hamou committed Jul 07, 2020 258 259 260 ``````Ltac trans b := apply Transitivity with (B := b); calc. Ltac thm := unfold IsTheorem; split; [ unfold Wf; split; [ auto | split; auto ] | ]. `````` Samuel Ben Hamou committed Jun 16, 2020 261 `````` `````` Samuel Ben Hamou committed Jul 02, 2020 262 263 264 265 266 267 ``````Ltac parse term := match term with | (_ -> ?queue)%form => parse queue | (∀ ?formula)%form => formula end. `````` Samuel Ben Hamou committed Jun 12, 2020 268 ``````Ltac rec := `````` Samuel Ben Hamou committed Jun 12, 2020 269 `````` match goal with `````` Samuel Ben Hamou committed Jul 02, 2020 270 271 `````` | |- exists axs, (Forall (IsAxiom PeanoTheory) axs /\ Pr ?l (axs ⊢ ?A))%type => let form := parse A in `````` Samuel Ben Hamou committed Jul 07, 2020 272 273 `````` exists (induction_schema form :: axioms_list); set (rec := induction_schema form); set (Γ := rec :: axioms_list); split; [ apply IsAx_adhoc; auto | `````` Samuel Ben Hamou committed Jul 02, 2020 274 `````` repeat apply R_Imp_i; `````` Samuel Ben Hamou committed Jul 07, 2020 275 `````` apply rec0_rule; calc ]; cbn `````` Samuel Ben Hamou committed Jun 16, 2020 276 `````` (* | _ => idtac *) `````` Samuel Ben Hamou committed Jun 12, 2020 277 `````` end. `````` Samuel Ben Hamou committed Jul 02, 2020 278 `````` `````` Samuel Ben Hamou committed Jun 16, 2020 279 `````` `````` 280 281 ``````(** Some basic proofs in Peano arithmetics. *) `````` Samuel Ben Hamou committed Jun 08, 2020 282 ``````Lemma ZeroRight : IsTheorem Intuiti PeanoTheory (∀ (#0 = #0 + Zero)). `````` Samuel Ben Hamou committed Jun 12, 2020 283 284 285 ``````Proof. thm. rec. `````` Samuel Ben Hamou committed Jul 07, 2020 286 287 288 289 `````` + sym. inst_axiom ax9 [Zero]. + app_R_All_i "y" y. apply R_Imp_i. set (H1 := _ = _). `````` Samuel Ben Hamou committed Jun 16, 2020 290 `````` sym. `````` Samuel Ben Hamou committed Jul 07, 2020 291 292 `````` trans (Succ (y + Zero)). - inst_axiom ax10 [y; Zero]. `````` Samuel Ben Hamou committed Jun 16, 2020 293 294 295 296 `````` - ahered. sym. apply R_Ax. apply in_eq. `````` Samuel Ben Hamou committed Jun 10, 2020 297 ``````Qed. `````` Samuel Ben Hamou committed Jun 08, 2020 298 `````` `````` 299 ``````Lemma SuccRight : IsTheorem Intuiti PeanoTheory (∀∀ (Succ(#1 + #0) = #1 + Succ(#0))). `````` Samuel Ben Hamou committed Jun 08, 2020 300 ``````Proof. `````` Samuel Ben Hamou committed Jun 16, 2020 301 302 `````` thm. rec. `````` Samuel Ben Hamou committed Jul 07, 2020 303 `````` + app_R_All_i "y" y. `````` Samuel Ben Hamou committed Jun 16, 2020 304 `````` sym. `````` Samuel Ben Hamou committed Jul 07, 2020 305 306 `````` trans (Succ y). - inst_axiom ax9 [Succ y]. `````` Samuel Ben Hamou committed Jun 16, 2020 307 308 `````` - ahered. sym. `````` Samuel Ben Hamou committed Jul 07, 2020 309 310 `````` inst_axiom ax9 [y]. + app_R_All_i "x" x. `````` Samuel Ben Hamou committed Jun 16, 2020 311 `````` apply R_Imp_i. `````` Samuel Ben Hamou committed Jul 07, 2020 312 `````` app_R_All_i "y" y. fold x. `````` Samuel Ben Hamou committed Jun 16, 2020 313 `````` set (hyp := ∀ Succ _ = _). `````` Samuel Ben Hamou committed Jul 07, 2020 314 `````` trans (Succ (Succ (x + y))). `````` Samuel Ben Hamou committed Jun 16, 2020 315 `````` - ahered. `````` Samuel Ben Hamou committed Jul 07, 2020 316 317 `````` inst_axiom ax10 [x; y]. - trans (Succ (x + Succ y)). `````` Samuel Ben Hamou committed Jun 16, 2020 318 `````` * ahered. `````` Samuel Ben Hamou committed Jul 07, 2020 319 320 321 `````` inst_axiom hyp [y]. * sym. inst_axiom ax10 [x; Succ y]. `````` Samuel Ben Hamou committed Jun 12, 2020 322 ``````Qed. `````` Samuel Ben Hamou committed Jul 07, 2020 323 `````` `````` Samuel Ben Hamou committed Jun 30, 2020 324 325 ``````Lemma Comm : IsTheorem Intuiti PeanoTheory `````` Samuel Ben Hamou committed Jul 02, 2020 326 327 `````` ((∀ #0 = #0 + Zero) -> (∀∀ Succ(#1 + #0) = #1 + Succ(#0)) -> (∀∀ #0 + #1 = #1 + #0)). `````` Samuel Ben Hamou committed Jun 30, 2020 328 ``````Proof. `````` Samuel Ben Hamou committed Jul 02, 2020 329 `````` thm. `````` Samuel Ben Hamou committed Jul 03, 2020 330 `````` rec; set (Γ' := _ :: _ :: Γ). `````` Samuel Ben Hamou committed Jul 07, 2020 331 332 `````` + app_R_All_i "x" x. trans x. `````` Samuel Ben Hamou committed Jul 03, 2020 333 `````` - sym. `````` Samuel Ben Hamou committed Jul 07, 2020 334 335 `````` assert (Pr Intuiti (Γ' ⊢ ∀ # 0 = # 0 + Zero)). { apply R_Ax. calc. } apply R_All_e with (t := x) in H; auto. `````` Samuel Ben Hamou committed Jul 03, 2020 336 `````` - sym. `````` Samuel Ben Hamou committed Jul 07, 2020 337 338 `````` inst_axiom ax9 [x]. + app_R_All_i "y" y. `````` Samuel Ben Hamou committed Jul 03, 2020 339 `````` apply R_Imp_i. `````` Samuel Ben Hamou committed Jul 07, 2020 340 341 `````` app_R_All_i "x" x. trans (Succ (x + y)). `````` Samuel Ben Hamou committed Jul 03, 2020 342 `````` - sym. `````` Samuel Ben Hamou committed Jul 07, 2020 343 344 345 346 `````` assert (Pr Intuiti ((∀ #0 + y = y + #0) :: Γ' ⊢ ∀ ∀ Succ (#1 + #0) = #1 + Succ (#0))). { apply R_Ax. calc. } apply R_All_e with (t := x) in H; auto. apply R_All_e with (t := y) in H; auto. - trans (Succ (y + x)). `````` Samuel Ben Hamou committed Jul 03, 2020 347 `````` * ahered. `````` Samuel Ben Hamou committed Jul 07, 2020 348 `````` assert (Pr Intuiti ((∀ #0 + y = y + #0) :: Γ' ⊢ ∀ #0 + y = y + #0)). { apply R_Ax. apply in_eq. } `````` Samuel Ben Hamou committed Jul 08, 2020 349 `````` apply R_All_e with (t := x) in H; auto. `````` Samuel Ben Hamou committed Jul 03, 2020 350 `````` * sym. `````` Samuel Ben Hamou committed Jul 07, 2020 351 `````` inst_axiom ax10 [y; x]. `````` Samuel Ben Hamou committed Jul 03, 2020 352 ``````Qed. `````` Samuel Ben Hamou committed Jun 08, 2020 353 `````` `````` Samuel Ben Hamou committed Jul 03, 2020 354 355 356 357 358 359 360 361 ``````Lemma Commutativity : IsTheorem Intuiti PeanoTheory (∀∀ #0 + #1 = #1 + #0). Proof. apply ModusPonens with (A := (∀∀ Succ(#1 + #0) = #1 + Succ(#0))). + apply ModusPonens with (A := ∀ #0 = #0 + Zero). * apply Comm. * apply ZeroRight. + apply SuccRight. Qed. `````` Samuel Ben Hamou committed Jul 07, 2020 362 `````` `````` Pierre Letouzey committed Aug 09, 2019 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 ``````(** 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 |}. Lemma PeanoAxOk A : IsAxiom PeanoTheory A -> forall genv, interp_form PeanoPreModel genv [] A. Proof. unfold PeanoTheory. simpl. unfold PeanoAx.IsAx. intros [IN|(B & -> & CK & CL)]. `````` Samuel Ben Hamou committed Jul 07, 2020 408 `````` - compute in IN. intuition; subst; cbn; intros; subst; omega. `````` Pierre Letouzey committed Aug 09, 2019 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 `````` - intros genv. unfold PeanoAx.induction_schema. apply interp_nforall. intros stk Len. rewrite app_nil_r. cbn. intros (Base,Step). (* The Peano induction emulated by a Coq induction :-) *) induction m. + specialize (Base 0). apply -> interp_form_bsubst_gen in Base; simpl; eauto. + apply Step in IHm. apply -> interp_form_bsubst_gen in IHm; simpl; eauto. now intros [|k]. Qed. Definition PeanoModel : Model nat PeanoTheory := {| pre := PeanoPreModel; AxOk := PeanoAxOk |}.``````