diff options
| author | Jasper Hugunin | 2020-10-09 15:53:47 -0700 |
|---|---|---|
| committer | Jasper Hugunin | 2020-10-11 19:05:14 -0700 |
| commit | 17ba1c432409cd84a83f29a5014b3597cfae9b03 (patch) | |
| tree | f549187cdca7877d6bf076fd81ef93328acffd61 | |
| parent | f136bcf5a067fcf1e38f48062ccde06875709e6a (diff) | |
Modify Arith/Even.v to compile with -mangle-names
| -rw-r--r-- | theories/Arith/Even.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Arith/Even.v b/theories/Arith/Even.v index 9c0a6bd96f..3422596818 100644 --- a/theories/Arith/Even.v +++ b/theories/Arith/Even.v @@ -39,28 +39,28 @@ Hint Constructors odd: arith. Lemma even_equiv : forall n, even n <-> Nat.Even n. Proof. fix even_equiv 1. - destruct n as [|[|n]]; simpl. + intros n; destruct n as [|[|n]]; simpl. - split; [now exists 0 | constructor]. - split. - + inversion_clear 1. inversion_clear H0. + + inversion_clear 1 as [|? H0]. inversion_clear H0. + now rewrite <- Nat.even_spec. - rewrite Nat.Even_succ_succ, <- even_equiv. split. - + inversion_clear 1. now inversion_clear H0. + + inversion_clear 1 as [|? H0]. now inversion_clear H0. + now do 2 constructor. Qed. Lemma odd_equiv : forall n, odd n <-> Nat.Odd n. Proof. fix odd_equiv 1. - destruct n as [|[|n]]; simpl. + intros n; destruct n as [|[|n]]; simpl. - split. + inversion_clear 1. + now rewrite <- Nat.odd_spec. - split; [ now exists 0 | do 2 constructor ]. - rewrite Nat.Odd_succ_succ, <- odd_equiv. split. - + inversion_clear 1. now inversion_clear H0. + + inversion_clear 1 as [? H0]. now inversion_clear H0. + now do 2 constructor. Qed. @@ -68,14 +68,14 @@ Qed. Lemma even_or_odd n : even n \/ odd n. Proof. - induction n. + induction n as [|n IHn]. - auto with arith. - elim IHn; auto with arith. Qed. Lemma even_odd_dec n : {even n} + {odd n}. Proof. - induction n. + induction n as [|n IHn]. - auto with arith. - elim IHn; auto with arith. Defined. |