Librairie lib_decimal (.sats)

(supprimer le menu, télécharger, aller au .dats)

(*******************************************************************)
(*                                                                 *)
(*        Functions about decimal representation of numbers        *)
(*                                                                 *)
(*******************************************************************)

(* Contains functions for palindromes, length of numbers, etc. *)


(***********************)
(*     Definitions     *)
(***********************)

(* Integers (≥ 0) are represented as lists of integers between 0 and 9, *least significant bit
  first* and without leading 0 *)

datasort intlist =
  | nil
  | cons of (int, intlist)

dataprop length_intlist (l : intlist, n : int) = // true iff n = length(l)
  | Nil_0 (nil, 0)
  | {t : intlist; n, h : int} Cons_length (cons (h, t), n + 1) of length_intlist (t, n)

dataprop int_to_intlist (n : int, l : intlist) = // true iff the decimal representation of n ≥ 0
  | Nil (0, nil)                                 // is l
  | {n : pos; l : intlist} Next (n, cons (n mod 10, l)) of int_to_intlist (n / 10, l)

propdef length_int (n : int, l : int) = // true iff n has length l
  [p : intlist] (int_to_intlist (n, p), length_intlist (p, l))

dataprop concat_list_list (l : intlist, m : intlist, r : intlist) = // true iff r = l @ m
  | {m : intlist} Bas (nil, m, m)
  | {h : int; l, m, r : intlist} Cons (cons (h, l), m, cons (h, r))
                                              of concat_list_list (l, m, r)

dataprop intlist_rev (l : intlist, r : intlist) = // true iff r = List.rev l
  | Nil_rev (nil, nil)
  | {h : int; t, r : intlist} Cons_rev (cons (h, t), r)
      of [l : intlist] (intlist_rev (t, l), concat_list_list (l, cons (h, nil), r))

propdef palindrome (n : int, m : int) = // true iff m is the reversed of n
  [l, l' : intlist] (int_to_intlist (n, l), int_to_intlist (m, l'), intlist_rev (l, l'))

propdef is_palindrome (n : int) = palindrome (n, n)

(******************)
(*     Proofs     *)
(******************)

// Axioms defining intlist equality

praxi intlist_eq_nil
        : [nil == nil] void

praxi intlist_eq_cons {x : int; l, m : intlist | l == m} ()
        : [cons (x, l) == cons (x, m)] void

praxi intlist_eq_tot {l, m : intlist | l == m} ()
        : [x : int; l', m' : intlist | l' == m']
            [(l == nil && m == nil) || (l == cons (x, l') && m == cons (x, m'))] void

// Basic properties

prfun intlist_eq_refl {l : intlist} () :<> [l == l] void

prfun intlist_eq_sym {l, m : intlist | l == m} () :<> [m == l] void

prfun intlist_eq_trans {l, m, n : intlist | l == m && m == n} () :<> [l == n] void


prfun int_to_intlist_istot {n : nat} (n : int n)
        :<> [l : intlist] int_to_intlist (n, l)

prfun concat_list_to_empty {l : intlist} ()
        : concat_list_list (l, nil, l)

prfun concat_istot {l, l' : intlist} ()
        :<> [r : intlist] (concat_list_list (l, l', r))

prfun concat_isfun {a, b, c, d : intlist}
                   (c : concat_list_list (a, b, c),
                    d : concat_list_list (a, b, d))
        : [c == d] void

prfun concat_isassoc {a, b, c, ab, bc, ab_c, a_bc : intlist}
                     (ab   : concat_list_list (a, b, ab),
                      bc   : concat_list_list (b, c, bc),
                      ab_c : concat_list_list (ab, c, ab_c),
                      a_bc : concat_list_list (a, bc, a_bc))
        : [ab_c == a_bc] void