Commit e8560422 authored by Johannes Kloos's avatar Johannes Kloos

Provide more Inj instances in numbers

parent 173b3078
...@@ -347,6 +347,14 @@ Proof. ...@@ -347,6 +347,14 @@ Proof.
Qed. Qed.
Close Scope Z_scope. Close Scope Z_scope.
(** * Injectivity of casts *)
Instance N_of_nat_inj: Inj (=) (=) N.of_nat := Nat2N.inj.
Instance nat_of_N_inj: Inj (=) (=) N.to_nat := N2Nat.inj.
Instance nat_of_pos_inj: Inj (=) (=) Pos.to_nat := Pos2Nat.inj.
Instance pos_of_Snat_inj: Inj (=) (=) Pos.of_succ_nat := SuccNat2Pos.inj.
Instance Z_of_N_inj: Inj (=) (=) Z.of_N := N2Z.inj.
(* Add others here. *)
(** * Notations and properties of [Qc] *) (** * Notations and properties of [Qc] *)
Open Scope Qc_scope. Open Scope Qc_scope.
Delimit Scope Qc_scope with Qc. Delimit Scope Qc_scope with Qc.
......
(* Copyright (c) 2012-2017, Coq-std++ developers. *) (* Copyright (c) 2012-2017, Coq-std++ developers. *)
(* This file is distributed under the terms of the BSD license. *) (* This file is distributed under the terms of the BSD license. *)
From stdpp Require Export strings. From stdpp Require Export strings.
From stdpp Require Import relations. From stdpp Require Import relations numbers.
From Coq Require Import Ascii. From Coq Require Import Ascii.
Set Default Proof Using "Type". Set Default Proof Using "Type".
...@@ -72,8 +72,5 @@ Instance pretty_Z : Pretty Z := λ x, ...@@ -72,8 +72,5 @@ Instance pretty_Z : Pretty Z := λ x,
end%string. end%string.
Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x). Instance pretty_nat : Pretty nat := λ x, pretty (N.of_nat x).
Instance pretty_nat_inj : Inj (@eq nat) (=) pretty. Instance pretty_nat_inj : Inj (@eq nat) (=) pretty.
Proof. Proof. apply _. Qed.
unfold pretty, pretty_nat.
apply compose_inj with (R2 := eq) (f := N.of_nat), _.
exact Nat2N.inj.
Qed.
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment