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