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.

  Parameter t : Set.
  Parameter toZ : t → Z.
  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 : Z → positive → t.

  Axiom truncate_on_zero :
    ∀ pwr, truncate_to_char 0 pwr = zero.

End CHAR.

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 : t → Z.
  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 : Z → t.
  Parameter const_prop : ∀ z,
   range z → toZ (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 y ⇒ false :: digits_of_pos y (Pos.pred p)
    | xI y ⇒ true :: digits_of_pos y (Pos.pred p)
    | xH ⇒ match p with
            | xH ⇒ true :: 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
      | Z0 ⇒ Pos.iter p addfalse nil
      | Zpos x1 ⇒ digits_of_pos x1 p
      | Zneg x1 ⇒ digits_of_pos ((Pos.pow 2 p ) - x1)%positive p
      end.

  Fixpoint pos_of_digits (d:list bool) : positive :=
  match d with
  | nil ⇒ xH
  | true :: nil ⇒ xH
  | false :: nil ⇒ xH
  | true :: tl ⇒ xI (pos_of_digits tl)
  | false :: tl ⇒ xO (pos_of_digits tl)
  end.
  Fixpoint clear_false (d:list bool) : list bool :=
  match d with
  | nil ⇒ nil
  | true :: tl ⇒ d
  | false :: tl ⇒ clear_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
  | nil ⇒ Z0
  | _ :: tl ⇒ match cf with
               | nil ⇒ Z0
               | _ :: _ ⇒ 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.