diff options
author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-10-10 16:54:37 +0200 |
---|---|---|
committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-10-10 16:54:37 +0200 |
commit | 8d4037118be3ffb7259ed03a5ba4ae09d9b51f4a (patch) | |
tree | 69b1ba6bbfeee1fa0b0f6ed847092d60a48e2f70 /src/versions/standard/Int63/Int63Op_standard.v | |
parent | a6cd7db941af0d41932fafc8104c3ee142b1c6f7 (diff) | |
download | smtcoq-8d4037118be3ffb7259ed03a5ba4ae09d9b51f4a.tar.gz smtcoq-8d4037118be3ffb7259ed03a5ba4ae09d9b51f4a.zip |
Some proofs for the Int63 glue
Diffstat (limited to 'src/versions/standard/Int63/Int63Op_standard.v')
-rw-r--r-- | src/versions/standard/Int63/Int63Op_standard.v | 40 |
1 files changed, 24 insertions, 16 deletions
diff --git a/src/versions/standard/Int63/Int63Op_standard.v b/src/versions/standard/Int63/Int63Op_standard.v index f34260c..d0df921 100644 --- a/src/versions/standard/Int63/Int63Op_standard.v +++ b/src/versions/standard/Int63/Int63Op_standard.v @@ -154,23 +154,24 @@ Definition existsb (f:int -> bool) from to := (* Definition to_Z := to_Z_rec size. *) Definition to_Z := phi. +Definition of_Z := phi_inv. + +(* Fixpoint of_pos_rec (n:nat) (p:positive) := *) +(* match n, p with *) +(* | O, _ => 0 *) +(* | S n, xH => 1 *) +(* | S n, xO p => (of_pos_rec n p) << 1 *) +(* | S n, xI p => (of_pos_rec n p) << 1 lor 1 *) +(* end. *) -Fixpoint of_pos_rec (n:nat) (p:positive) := - match n, p with - | O, _ => 0 - | S n, xH => 1 - | S n, xO p => (of_pos_rec n p) << 1 - | S n, xI p => (of_pos_rec n p) << 1 lor 1 - end. - -Definition of_pos := of_pos_rec size. +(* Definition of_pos := of_pos_rec size. *) -Definition of_Z z := - match z with - | Zpos p => of_pos p - | Z0 => 0 - | Zneg p => - (of_pos p) - end. +(* Definition of_Z z := *) +(* match z with *) +(* | Zpos p => of_pos p *) +(* | Z0 => 0 *) +(* | Zneg p => - (of_pos p) *) +(* end. *) (** Gcd **) Fixpoint gcd_rec (guard:nat) (i j:int) {struct guard} := @@ -250,7 +251,7 @@ Definition cast_digit d1 d2 : | _, _ => None end. -(* TODO: improve this definition... *) +(* May need to improve this definition, but no reported efficiency problem for the moment *) Definition cast i j : option (forall P : int -> Type, P i -> P j) := match i, j return option (forall P : int -> Type, P i -> P j) with @@ -331,3 +332,10 @@ Definition eqo i j : option (i = j) := | Some k => Some (k (fun j => i = j) (refl_equal i)) | None => None end. + + +(* + Local Variables: + coq-load-path: ((rec "../../.." "SMTCoq")) + End: +*) |