Library Char

Common interface for character domains.
@author Aleksy Schubert based on the Numeric module of Bicolano
Require Export ZArith BinPosDef BinNums.
Require Import Common List.
Import List.ListNotations.

Open Local Scope Z_scope.

Signature

Signature for modules implementing characters.
Module Type CHAR.

Original Bicolano staff

  Parameter t : Set.
  Parameter toZ : tZ.
  Parameter power : Z.
  Parameter power_positive: power > 0.
  Parameter zero : t.
  Axiom PzeroToZ: toZ zero = 0.
  Definition base := 2^power.
  Definition range (z:Z) : Prop := 0 z < base.
  Parameter range_prop : x:t, range (toZ x).

The operation to truncate a number in the representation given by the second argument to the representation given by the current module
  Parameter truncate_to_char : Zpositivet.

  Axiom truncate_on_zero :
     pwr, truncate_to_char 0 pwr = zero.

End CHAR.

Implementation

Provides power parameter for NUMERIC module.
Module Type CHARSIZE.
  Parameter power : Z.
  Parameter power_positive: power > 0.

End CHARSIZE.

Creates an actual module implementing NUMERIC for a given power. In fact, the implementation is incomplete (some Parameters and Axioms left).
Module Make (S:CHARSIZE) : CHAR with Definition power := S.power.
  Parameter t : Set.
  Parameter toZ : tZ.
  Definition power := S.power.
  Definition base := 2^power.
  Definition range (z:Z) : Prop := 0 z < base.
  Parameter range_prop : x:t, range (toZ x).
  Lemma power_positive : power > 0.
  Proof.
    apply S.power_positive.
  Qed.
  Parameter const : Zt.
  Parameter const_prop : z,
   range ztoZ (const z) = z.

  Lemma base_ge_2: 2 base.
  Proof.
    unfold base.
    change (2^1 2^power).
    apply Z.pow_le_mono.
    omega.
    assert (H := power_positive).
    omega.
  Qed.

  Definition zero : t := const 0.
  Lemma PzeroToZ: toZ zero = 0.
  Proof.
    apply const_prop.
    unfold range.
    assert (H := base_ge_2).
    omega.
  Qed.

Transforms the given positive x into its list of least significant bits according to the representation in p bits

  Fixpoint digits_of_pos (x:positive) (p:positive) : list bool :=
     let addfalse li := false :: li in
    match x with
    | xO yfalse :: digits_of_pos y (Pos.pred p)
    | xI ytrue :: digits_of_pos y (Pos.pred p)
    | xHmatch p with
            | xHtrue :: nil
            | _true :: Pos.iter (Pos.pred p) addfalse nil
            end
    end.

Lemma testdop45 : (digits_of_pos 4 5) = [false; false; true; false; false].
Proof.
simpl.
trivial.
Qed.

Transforms the given integer x into its list of least significant bits according to the representation in p bits
  Fixpoint digits_of_Z (x:Z) (p:positive) : list bool :=
    let addfalse li := false :: li in
      match x with
      | Z0Pos.iter p addfalse nil
      | Zpos x1digits_of_pos x1 p
      | Zneg x1digits_of_pos ((Pos.pow 2 p) - x1)%positive p
      end.

  Fixpoint pos_of_digits (d:list bool) : positive :=
  match d with
  | nilxH
  | true :: nilxH
  | false :: nilxH
  | true :: tlxI (pos_of_digits tl)
  | false :: tlxO (pos_of_digits tl)
  end.
  Fixpoint clear_false (d:list bool) : list bool :=
  match d with
  | nilnil
  | true :: tld
  | false :: tlclear_false tl
  end.

TODO we assume d is unsigned
  Fixpoint pos_Z_of_digits (d:list bool) : Z :=
  let rl := rev d in
  let cf := clear_false rl in
  match rl with
  | nilZ0
  | _ :: tlmatch cf with
               | nilZ0
               | _ :: _Zpos (pos_of_digits (rev cf))
               end
  end.

  Definition truncateZ (x:Z) (p:positive) : Z :=
    pos_Z_of_digits (firstn (Z.to_nat power) (digits_of_Z x p)).

  Definition truncate_to_char (x:Z) (p:positive) : t := const (truncateZ x p).

Lemma testm75 : power = 5 → (truncateZ (-7) 5) = 25.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  trivial.
Qed.

Lemma testm74 : power = 4 → (truncateZ (-7) 5) = 9.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  simpl.
  trivial.
Qed.

Lemma testm73 : power = 3 → (truncateZ (-7) 5) = 1.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  trivial.
Qed.

Lemma testm45 : power = 5 → (truncateZ 4 5) = 4.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  simpl.
  trivial.
Qed.

Lemma testm44 : power = 5 → (truncateZ 4 4) = 4.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  simpl.
  trivial.
Qed.

Lemma testm43 : power = 2 → (truncateZ 4 5) = 0.
Proof.
  intros.
  unfold truncateZ.
  rewrite H.
  trivial.
Qed.

  Axiom truncate_on_zero :
     pwr, truncate_to_char 0 pwr = zero.

End Make.