text:
From Hammer Require Import Hammer.

From compcert Require Import Raux.
From compcert Require Import Defs.
From compcert Require Import Round_pred.
From compcert Require Import Generic_fmt.
From compcert Require Import Ulp.
From compcert Require Import Round_NE.

Section RND_FIX.

Variable beta : radix.

Notation bpow := (bpow beta).

Variable emin : Z.

Inductive FIX_format (x : R) : Prop :=
FIX_spec (f : float beta) :
x = F2R f -> (Fexp f = emin)%Z -> FIX_format x.

Definition FIX_exp (e : Z) := emin.

Global Instance FIX_exp_valid : Valid_exp FIX_exp.
Proof. hammer_hook "FIX" "FIX.FIX_exp_valid".
intros k.
unfold FIX_exp.
split ; intros H.
now apply Zlt_le_weak.
split.
apply Z.le_refl.
now intros _ _.
Qed.

Theorem generic_format_FIX :
forall x, FIX_format x -> generic_format beta FIX_exp x.
Proof. hammer_hook "FIX" "FIX.generic_format_FIX".
intros x [[xm xe] Hx1 Hx2].
rewrite Hx1.
now apply generic_format_canonical.
Qed.

Theorem FIX_format_generic :
forall x, generic_format beta FIX_exp x -> FIX_format x.
Proof. hammer_hook "FIX" "FIX.FIX_format_generic".
intros x H.
rewrite H.
eexists ; repeat split.
Qed.

Theorem FIX_format_satisfies_any :
satisfies_any FIX_format.
Proof. hammer_hook "FIX" "FIX.FIX_format_satisfies_any".
refine (satisfies_any_eq _ _ _ (generic_format_satisfies_any beta FIX_exp)).
intros x.
split.
apply FIX_format_generic.
apply generic_format_FIX.
Qed.

Global Instance FIX_exp_monotone : Monotone_exp FIX_exp.
Proof. hammer_hook "FIX" "FIX.FIX_exp_monotone".
intros ex ey H.
apply Z.le_refl.
Qed.

Theorem ulp_FIX :
forall x, ulp beta FIX_exp x = bpow emin.
Proof. hammer_hook "FIX" "FIX.ulp_FIX".
intros x; unfold ulp.
case Req_bool_spec; intros Zx.
case (negligible_exp_spec FIX_exp).
intros T; specialize (T (emin-1)%Z); contradict T.
unfold FIX_exp; omega.
intros n _; reflexivity.
reflexivity.
Qed.

End RND_FIX.

author: lukaszcz

repo: coqhammer-eval


text:
(**                                                                                *)
(**                             The SQLEngines Library                              *)
(**                                                                                *)
(**            LRI, CNRS & Université Paris-Sud, Université Paris-Saclay            *)
(**                                                                                *)
(**                        Copyright 2016-2019 : FormalData                         *)
(**                                                                                *)
(**         Authors: Véronique Benzaken                                             *)
(**                  Évelyne Contejean                                              *)
(**                  Chantal Keller                                                 *)
(**                  Eunice-Raquel Martins                                          *)
(**                                                                                *)
(************************************************************************************)

Set Implicit Arguments.

Require Import Relations SetoidList List String Ascii Bool ZArith NArith.

Require Import FlatData ListFacts OrderedSet
        FiniteSet FiniteBag FiniteCollection Tree Formula SqlCommon SqlAlgebra.

Import Tuple.
Require Import Values Relnames SortedAttributes SortedTuples.

(** Defining functions and aggregates, and giving their interpretation *)

Inductive symbol : Type :=
  | Symbol : string -> symbol
  | CstVal : value -> symbol.

Inductive predicate : Type := Predicate : string -> predicate.

Definition OP : Oset.Rcd predicate.
split with (fun x y => match x, y with Predicate s1, Predicate s2 => string_compare s1 s2 end).
- intros [s1] [s2]; generalize (Oset.eq_bool_ok Ostring s1 s2); simpl.
  case (string_compare s1 s2).
  + apply f_equal.
  + intros H1 H2; apply H1; injection H2; exact (fun h => h).
  + intros H1 H2; apply H1; injection H2; exact (fun h => h).
- intros [s1] [s2] [s3]; apply (Oset.compare_lt_trans Ostring s1 s2 s3).
- intros [s1] [s2]; apply (Oset.compare_lt_gt Ostring s1 s2).
Defined.

Definition symbol_compare (s1 s2 : symbol) :=
  match s1, s2 with
    | Symbol s1, Symbol s2 => string_compare s1 s2
    | Symbol _, CstVal _ => Lt
    | CstVal _, Symbol _ => Gt
    | CstVal v1, CstVal v2 => value_compare v1 v2
  end.

Definition OSymbol : Oset.Rcd symbol.
split with symbol_compare.
- intros [s1 | s1] [s2 | s2]; simpl; try discriminate.
  + generalize (Oset.eq_bool_ok Ostring s1 s2); simpl.
    case (string_compare s1 s2).
    * apply f_equal.
    * intros H1 H2; apply H1; injection H2; exact (fun h => h).
    * intros H1 H2; apply H1; injection H2; exact (fun h => h).
  + generalize (Oset.eq_bool_ok OVal s1 s2); simpl.
    case (value_compare s1 s2).
    * apply f_equal.
    * intros H1 H2; apply H1; injection H2; exact (fun h => h).
    * intros H1 H2; apply H1; injection H2; exact (fun h => h).
- intros [s1 | s1] [s2 | s2] [s3 | s3]; simpl;
  try (apply (Oset.compare_lt_trans Ostring) ||
             apply (Oset.compare_lt_trans OVal) ||
             trivial || discriminate).
- intros [s1 | s1] [s2 | s2]; simpl;
  try (apply (Oset.compare_lt_gt Ostring) ||
             apply (Oset.compare_lt_gt OVal) ||
             trivial || discriminate).
Defined.

Require Import compcert.lib.Integers.

Definition interp_symbol f :=
  match f with
    | Symbol "plus" =>
      fun l =>
        match l with
          | Value_ptrofs a1 :: Value_ptrofs a2 :: nil => Value_ptrofs (Ptrofs.add a1 a2)
          | _ => Value_ptrofs Ptrofs.zero end
    | Symbol "mult" =>
      fun l =>
        match l with
          | Value_ptrofs a1 :: Value_ptrofs a2 :: nil => Value_ptrofs (Ptrofs.mul a1 a2)
          | _ => Value_ptrofs Ptrofs.zero end
    | Symbol "minus" =>
      fun l =>
        match l with
          | Value_ptrofs a1 :: Value_ptrofs a2 :: nil => Value_ptrofs (Ptrofs.sub a1 a2)
          | _ => Value_ptrofs Ptrofs.zero end
    | Symbol "opp" =>
      fun l =>
        match l with
          | Value_ptrofs a1 :: nil => Value_ptrofs (a1 (* ? *))
          | _ => Value_ptrofs Ptrofs.zero end
    | CstVal v =>
      fun l =>
        match l with
          | nil => v
          | _ => default_value (type_of_value v)
        end
    | _ => fun _ => Value_ptrofs Ptrofs.zero
  end.

Definition interp_predicate p :=
  match p with
    | Predicate "<" =>
      fun l =>
        match l with
          | Value_ptrofs a1 :: Value_ptrofs a2 :: nil =>
            match ptrofs_compare a1 a2 with Lt => true | _ => false end
          | _ => false
        end
    | Predicate "<=" =>
      fun l =>
        match l with
          | Value_ptrofs a1 :: Value_ptrofs a2 :: nil =>
            match ptrofs_compare a1 a2 with Gt => false | _ => true end
          | _ => false
        end

    | Predicate ">" =>
      fun l =>
        match l with
          | Value_ptrofs a1 :: Value_ptrofs a2 :: nil =>
            match ptrofs_compare a1 a2 with Gt => true | _ => false end
          | _ => false
        end

    | Predicate ">=" =>
      fun l =>
        match l with
          | Value_ptrofs a1 :: Value_ptrofs a2 :: nil =>
            match ptrofs_compare a1 a2 with Lt => false | _ => true end
          | _ => false
        end

    | Predicate "=" =>
      fun l =>
        match l with
          | Value_ptrofs a1 :: Value_ptrofs a2 :: nil =>
            match ptrofs_compare a1 a2 with Eq => true | _ => false end
          | Value_string s1 :: Value_string s2 :: nil =>
            match string_compare s1 s2 with Eq => true | _ => false end
          | _ => false
        end
   | _ => fun _ => false
  end.

Inductive aggregate : Type :=
  | Aggregate : string -> aggregate.

Definition OAgg : Oset.Rcd aggregate.
split with (fun x y => match x, y with Aggregate s1, Aggregate s2 => string_compare s1 s2 end).
- intros [s1] [s2]; generalize (Oset.eq_bool_ok Ostring s1 s2); simpl.
  case (string_compare s1 s2).
  + apply f_equal.
  + intros H1 H2; apply H1; injection H2; exact (fun h => h).
  + intros H1 H2; apply H1; injection H2; exact (fun h => h).
- intros [s1] [s2] [s3]; apply (Oset.compare_lt_trans Ostring s1 s2 s3).
- intros [s1] [s2]; apply (Oset.compare_lt_gt Ostring s1 s2).
Defined.

Definition interp_aggregate a := fun l =>
  match a with
    | Aggregate "count" => Value_ptrofs (Ptrofs.of_int (Int.repr (Zlength l)))
    | Aggregate "sum" =>
      Value_ptrofs
        (fold_left (fun acc x => match x with Value_ptrofs x => (Ptrofs.add acc x)%N | _ => acc end) l Ptrofs.zero)
    | Aggregate "avg" =>
      Value_ptrofs
        (let sum :=
                   fold_left (fun acc x => match x with
                                           | Value_ptrofs x => (Ptrofs.add acc x)%N
                                           | _ => acc end) l Ptrofs.zero in
               Ptrofs.divu sum (Ptrofs.of_int (Int.repr (Zlength l))))
    | Aggregate _ => Value_ptrofs Ptrofs.zero
  end.

(** Building a database instance, and updating it  *)
Definition mk_tuple la f := mk_tuple T (Fset.mk_set FAN la) f.

Definition show_tuple t :=
  List.map
    (fun a => (a, dot T t a))
    (Fset.elements _ (support _ t)).

Definition show_bag_tuples x :=
  List.map show_tuple (Febag.elements (Fecol.CBag (CTuple T)) x).

Definition show_col_tuples x :=
  List.map show_tuple (Fecol.elements (CA := CTuple T) x).

Record db_state : Type :=
  mk_state
    {
      _relnames : list relname;
      _basesort : relname -> Fset.set FAN;
      _instance : relname -> Febag.bag (Fecol.CBag (CTuple T))
    }.

Definition show_state (db : db_state) :=
  (_relnames db,
   List.map (fun r => (r, Fset.elements _ (_basesort db r))) (_relnames db),
   List.map (fun r => (r, show_bag_tuples (_instance db r))) (_relnames db)).

Definition init_db :=
  mk_state
    nil
    (fun _ => Fset.empty FAN)
    (fun _ => Febag.empty (Fecol.CBag (CTuple T))).

Definition create_table
           (* old state *) db
           (* new table name *) t
           (* new table sort *) st
            :=
  mk_state
    (t :: _relnames db)
    (fun x =>
       match Oset.compare ORN x t with
         | Eq => Fset.mk_set FAN st
         |_ => _basesort db x
       end)
    (_instance db).

Definition insert_tuple_into
           (* old state *) db
           (* new tuple *) tpl
           (* table *) tbl
            :=
  mk_state
    (_relnames db)
    (_basesort db)
    (fun x =>
       match Oset.compare ORN x tbl with
       | Eq => Febag.add (Fecol.CBag (CTuple T)) tpl (_instance db tbl)
       |_ => _instance db x
       end).

Fixpoint insert_tuples_into
           (* old state *) db
           (* new tuple list *) ltpl
           (* table *) tbl :=
  match ltpl with
    | nil => db
    | t :: l => insert_tuple_into (insert_tuples_into db l tbl) t tbl
  end.

Definition MyDBS db := DatabaseSchema.mk_R (Tuple.A T) ORN (_basesort db).

Definition db0 := init_db.

Notation year := (Attr_ptrofs 0 "year").
Notation firstname := (Attr_string 0 "firstname").
Notation lastname := (Attr_string 0 "lastname").
Notation title := (Attr_string 0 "title").
Notation name := (Attr_string 0 "name").
Notation r_mid := (Attr_ptrofs 0 "r.mid").
Notation runtime := (Attr_ptrofs 0 "runtime").
Notation rank := (Attr_ptrofs 0 "rank").
Notation r_pid := (Attr_ptrofs 0 "r.pid").
Notation d_mid := (Attr_ptrofs 0 "d.mid").
Notation d_pid := (Attr_ptrofs 0 "d.pid").
Notation p_pid := (Attr_ptrofs 0 "p.pid").
Notation m_mid := (Attr_ptrofs 0 "m.mid").

(* role: mid, pid, name *)
Definition mk_role mid pid n :=
  mk_tuple
    (r_mid :: r_pid :: nil)
    (fun a => match a with
              | r_mid => Value_ptrofs (Ptrofs.of_int (Int.repr mid))
              | r_pid => Value_ptrofs (Ptrofs.of_int (Int.repr pid))
              | name => Value_string n
              | Attr_string _ _ => Value_string ""
              | Attr_ptrofs _ _ => Value_ptrofs Ptrofs.zero
              end) base.nullval.

Definition roles :=
  mk_role 2120 640 "Man with Knife"
    :: mk_role 2120 715 "J.J. Gittes"
    :: mk_role 2279 2330 "Cliff Stern"
    :: mk_role 2279 874 "Judah Rosenthal"
    :: mk_role 2406 4970 "Shrek"
    :: mk_role 2406 4972 "Princess Fiona"
    :: mk_role 2139 1805 "'Maxim' de Winter"
    :: mk_role 2139 1806 "Mrs. de Winter"
    :: nil.

(* director: mid, pid *)
Definition mk_director mid pid :=
  mk_tuple
    (d_mid :: d_pid :: nil)
    (fun a => match a with
              | d_mid => Value_ptrofs (Ptrofs.of_int (Int.repr mid))
              | d_pid => Value_ptrofs (Ptrofs.of_int (Int.repr pid))
              | Attr_string _ _ => Value_string ""
              | Attr_ptrofs _ _ => Value_ptrofs Ptrofs.zero
              end) base.nullval.

Definition directors :=
  mk_director 2120 640
    :: mk_director 2279 2330
    :: mk_director 2406 4969
    :: mk_director 2139 464
    :: nil.

(* movie: mid, title, year, runtime, rank *)
Definition mk_movie mid t y rt rk :=
  mk_tuple
    (m_mid :: title :: year :: nil)
    (fun a => match a with
              | m_mid => Value_ptrofs (Ptrofs.of_int (Int.repr mid))
              | title => Value_string t
              | year => Value_ptrofs (Ptrofs.of_int (Int.repr y))
              | runtime => Value_ptrofs (Ptrofs.of_int (Int.repr rt))
              | rank => Value_ptrofs (Ptrofs.of_int (Int.repr rk))
              | Attr_string _ _ => Value_string ""
              | Attr_ptrofs _ _ => Value_ptrofs Ptrofs.zero
              end) base.nullval.

Definition movies :=
  mk_movie 2120 "Chinatown" 1974 130 121
    :: mk_movie 2279 "Crimes and Misdemeanors" 1989 104 280
    :: mk_movie 2406 "Shrek" 2001 90 407
    :: mk_movie 2139 "Rebecca" 1940 130 140
    :: nil.

(* people: pid, firstname, lastname *)
Definition mk_people pid f l :=
  mk_tuple
    (p_pid :: lastname :: nil)
    (fun a => match a with
              | p_pid => Value_ptrofs (Ptrofs.of_int (Int.repr pid))
              | firstname => Value_string f
              | lastname => Value_string l
              | Attr_string _ _ => Value_string ""
              | Attr_ptrofs _ _ => Value_ptrofs Ptrofs.zero
              end) base.nullval.

Definition people :=
  mk_people 640 "Roman" "Polanski"
    :: mk_people 715 "Jack" "Nicholson"
    :: mk_people 2330 "Woody" "Allen"
    :: mk_people 874 "Martin" "Landau"
    :: mk_people 4970 "Mike" "Myers"
    :: mk_people 4972 "Cameron" "Diaz"
    :: mk_people 1805 "Laurence" "Olivier"
    :: mk_people 1806 "Joan" "Fontaine"
    :: mk_people 4969 "Vicky" "Jenson"
    :: mk_people 464 "Alfred" "Hitchcock"
    :: nil.

Definition create_schema :=
create_table
  (create_table
     (create_table
        (create_table db0 (Rel "role") (r_mid :: r_pid :: name :: nil))
        (Rel "director") (d_mid :: d_pid :: nil))
     (Rel "people") (p_pid :: firstname :: lastname :: nil))
  (Rel "movie") (m_mid :: title :: year :: runtime :: rank :: nil).

Definition create_db roles directors people movies :=
  insert_tuples_into
    (insert_tuples_into
       (insert_tuples_into
          (insert_tuples_into create_schema movies (Rel "movie"))
          people (Rel "people"))
       directors (Rel "director"))
    roles (Rel "role").

Definition db1 := create_db roles directors people movies.

Require Import Signatures SeqScan HashIndexScan IndexJoin Filter QEP.

Module TPL <: TUPLE.
  Definition T := T.
End TPL.

Module QEP := QEP TPL.

Definition show c :=
   (map show_tuple (Cursor.materialize _ (QEP.eval_cursor c))).

(* The QEP *)
Definition seq_scan_on_role := QEP.SeqScan roles.

Definition hash_and_seq_scan_on_director :=
  QEP.SimpleHashIndexScan (d_mid :: d_pid :: nil) directors.

Definition hash_join :=
  QEP.IndexJoin (r_mid :: r_pid :: nil) seq_scan_on_role hash_and_seq_scan_on_director.

(* Projection for people: (p_pid, firstname, lastname) -> (p_pid) *)
Definition index_scan_on_people :=
  QEP.SimpleHashIndexScan (p_pid :: nil) people.

(* Projection for the deeper Index Join: (d_mid, d_pid, r_mid, r_pid) -> (d_pid) *)
Definition deeper_index_join :=
  QEP.IndexJoin (d_pid :: nil) hash_join index_scan_on_people.

(* Filter for movie year > 1950 *)
Definition theta_movie (x : tuple T) : bool :=
  match dot _ x year with
  | Value_ptrofs y => Ptrofs.lt (Ptrofs.of_int (Int.repr 1950)) y
  | _ => false
  end.

Lemma htheta_movie s f p1 p2:
  theta_movie (Tuple.mk_tuple _ s f p1) = theta_movie (Tuple.mk_tuple _ s f p2).
Proof.
  unfold theta_movie.
  unfold dot, dot_. simpl. unfold Tuple1.support, Tuple1.abs.
  simpl. reflexivity.
Qed.

(* Projection for movie: (m_mid, title, year, runtime, rank) -> (m_mid) *)
Definition index_scan_on_movie :=
  QEP.FilterHashIndexScan theta_movie htheta_movie (m_mid :: nil) movies.

(* Projection for the shallower Index Join:
  (lastname, d_mid, d_pid, p_pid, r_mid, r_pid) -> d_mid) *)
Definition qep :=
  QEP.IndexJoin (d_mid :: nil) deeper_index_join index_scan_on_movie.

(* Cannot compute *)
(* Definition qep_run :=
  Eval compute in (map show_tuple (Cursor.materialize _ (QEP.eval_cursor qep))).
Print qep_run. *)

author: PrincetonUniversity

repo: DeepSpecDB


text:
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import XRbase.
Require Import XRfunctions.
Require Import XSeqSeries.
Local Open Scope XR_scope.

(*****************************************************************)
(**           To define transcendental functions                 *)
(**           and exponential function                           *)
(*****************************************************************)

(*********)

Lemma mixup : forall x n, R0 < x -> (Z.to_nat ( up x) <= n)%nat -> IZR (up x) <= INR n.
Proof.
intros x n hx h.
destruct (archimed x) as [ al ar ].
apply inj_le in h.
rewrite Z2Nat.id in h.
2:{
  apply le_IZR.
  change (IZR 0) with R0.
  apply Rle_trans with x.
  left. assumption.
  left. assumption.
}
apply IZR_le in h.
rewrite INR_IZR_INZ.
exact h.
Qed.

Lemma Alembert_exp :
  Un_cv (fun n:nat => Rabs (/ INR (fact (S n)) * / / INR (fact n))) R0.
Proof.
  unfold Un_cv.
  intros e he.
  unfold R_dist.
  unfold Rminus.
  rewrite Ropp_0.

  set (Nr := / e).

  exists (Z.to_nat (up Nr)).
  intros n hn.

  rewrite Rplus_0_r.
  rewrite Rabs_mult.
  rewrite Rabs_mult.
  rewrite Rabs_Rabsolu.
  rewrite Rabs_Rabsolu.
  rewrite Rinv_involutive.
  2:{
    apply Rlt_not_eq'.
    change R0 with (INR 0%nat).
    apply lt_INR.
    apply lt_O_fact.
  }
  rewrite Rabs_Rinv.
  2:{
    apply Rlt_not_eq'.
    change R0 with (INR 0%nat).
    apply lt_INR.
    apply lt_O_fact.
  }
  rewrite Rmult_comm.
  rewrite Rabs_right.
  2:{
    change R0 with (INR 0%nat).
    left.
    apply lt_INR.
    apply lt_O_fact.
  }
  rewrite Rabs_right.
  2:{
    change R0 with (INR 0%nat).
    left.
    apply lt_INR.
    apply lt_O_fact.
  }
  simpl.
  rewrite plus_INR.
  rewrite mult_INR.
  set (f:=INR(fact n)).
  pattern f at 2;rewrite <- Rmult_1_l.
  rewrite <- Rmult_plus_distr_r.
  rewrite Rinv_mult_distr.
  rewrite <- Rmult_assoc.
  rewrite Rmult_comm.
  rewrite <- Rmult_assoc.
  rewrite Rinv_l.
  rewrite Rmult_1_l.
  2:{
    unfold f.
    change R0 with (INR 0%nat).
    apply Rlt_not_eq'.
    apply lt_INR.
    apply lt_O_fact.
  }
  2:{
    apply Rlt_not_eq'.
    apply Rlt_le_trans with R1.
    exact Rlt_0_1.
    pattern R1 at 1;rewrite <- Rplus_0_r.
    apply Rplus_le_compat_l.
    change R0 with (INR 0%nat).
    apply le_INR.
    apply le_0_n.
  }
  2:{
    unfold f.
    change R0 with (INR 0%nat).
    apply Rlt_not_eq'.
    apply lt_INR.
    apply lt_O_fact.
  }
  clear f.
  destruct (archimed Nr) as [al ar].
  unfold Nr in *. clear Nr.
  rewrite <- (Rinv_involutive e).
  2:{ apply Rlt_not_eq'. exact he. }
  apply Rinv_lt_contravar.
  {
    apply Rmult_lt_0_compat.
    { apply Rinv_0_lt_compat. exact he. }
    { apply Rlt_le_trans with R1.
      { exact Rlt_0_1. }
      {
        pattern R1 at 1;rewrite <- Rplus_0_r.
        apply Rplus_le_compat_l.
        change R0 with (INR 0).
        apply le_INR.
        apply le_0_n.
      }
    }
  }
  unfold ge in hn.
  apply Rlt_le_trans with (IZR (up (/ e))).
  { exact al. }
  apply Rplus_le_reg_r with (- / e).
  apply Rle_trans with R1.
  exact ar.
  apply Rplus_le_reg_r with (/ e).
  repeat rewrite Rplus_assoc.
  rewrite Rplus_opp_l, Rplus_0_r.
  apply Rplus_le_compat_l.
  apply Rle_trans with (IZR (up (/ e))).
  left. exact al.
  apply mixup.
  apply Rinv_0_lt_compat. exact he.
  exact hn.
Qed.

author: xavierdpt

repo: research

save_path: github-repos/coq/xavierdpt-research


text:
(*****************************************************************************)
(*                                                                           *)
(*  Domain.v                                                                 *)
(*                                                                           *)
(*  Tensors will be modelled as total maps from finite domains to the reals  *)
(*  (or, more generally, to a field or ring). This file models the relevant  *)
(*  finite domains as tuples of bounded natural numbers.                     *)
(*                                                                           *)
(*  Bijections between finite domains are also defined. These bijections     *)
(*  will be used to define the transposition operation on tensors. More      *)
(*  generally, bijections can be used to define what is usually called a     *)
(*  'reshape' or a 'view' of a tensor.                                       *)
(*                                                                           *)
(*****************************************************************************)

Require Import Basics.
Require Import Eqdep_dec.
Require Import FunctionalExtensionality.

Require Import TensorIR.Equations.Shallow.Vectors.

Import VectorNotations.

Definition Fin := Fin.t.

(* The type of a finite domain (of a tensor) is
   a tuple of types of bounded natural numbers: *)

Fixpoint DomainT {r : nat} (bounds : NVect r) : Set :=
  match bounds with
    | [] => unit
    | d::bound' => ((Fin d) * (DomainT bound'))%type
  end.

(* Equality of domains is decidable: *)

Lemma dom_eq_dec {n : nat} {b : NVect n} :
  forall (x y : DomainT b), {x = y} + {x <> y}.
Proof with auto.
  induction b; destruct x, y...
  destruct (IHb d d0) as [IHeq | IHneq];
    destruct (Fin.eq_dec f f0) as [FinEq | FinNeq].
  2-4: right; inversion 1...
  left; rewrite IHeq; rewrite FinEq...
Qed.

(* "Unicity of identity proofs" for domains: *)

Lemma dom_UIP_dec {n : nat} {b : NVect n} :
  forall (x : DomainT b) (pf1 pf2 : x = x), pf1 = pf2.
Proof.
  intros x pf; apply (UIP_dec dom_eq_dec).
Qed.

Lemma dom_UIP_refl {n : nat} {b : NVect n} :
  forall (x : DomainT b) (pf : x = x), pf = eq_refl x.
Proof.
  intros x pf; apply dom_UIP_dec.
Qed.

(* Two alternative definitions for splitting of tuples: *)

Fixpoint split' (l : nat) {r : nat} {b : NVect (l + r)}
                (i : DomainT b) {struct l} :
                DomainT (fst (splitat l b))* DomainT (snd (splitat l b)).
  refine(match l as l0
                 return (forall (b0 : NVect (l0 + r)),
                         DomainT b0 ->
                         DomainT (fst (splitat l0 b0))
                         * DomainT (snd (splitat l0 b0)))
         with
           | 0    => fun _ i => (tt,i)
           | S l' => fun b' i => _
         end b i).
Proof.
  destruct (splitat l' (tl b')) as (b0,bs) eqn:Heq.
  rewrite (eta b') in i; simpl in i.
  pose proof (split' l' r (tl b') (snd i)) as H; rewrite Heq in H; simpl in H.
  simpl; rewrite Heq; exact ((fst i, fst H), snd H).
Defined.

Fixpoint split (l : nat) {r : nat} {b0 : NVect l} {b1 : NVect r} {struct b0} :
               DomainT (b0 ++ b1) -> DomainT b0 * DomainT b1 :=
  match b0 as b0'
           return (DomainT (b0' ++ b1) -> DomainT b0' * DomainT b1)
  with
    | [] => fun i => (tt,i)
    | b00::b0'' => fun i => let (i0,i') := i in
                            let (j0,j1) := split _ i' in
                            ((i0,j0),j1)
  end.

(* Concatenation of tuples: *)

Fixpoint dom_append {m n : nat} {b0 : NVect m} {b1 : NVect n} :
  DomainT b0 -> DomainT b1 -> DomainT (b0 ++ b1) :=
    match b0 as b0'
             return (DomainT b0' -> DomainT b1 -> DomainT (b0' ++ b1))
    with
      | [] => fun _ i1 => i1
      | d::b0'' => fun i0 i1 => let (i00,i0') := i0 in
                                let tl := dom_append i0' i1 in
                                (i00,tl)
    end.

Lemma dom_split_append {r0 r1 : nat} {b0 : NVect r0} {b1 : NVect r1} :
  forall (j0 : DomainT b0) (j1 : DomainT b1),
    split r0 (dom_append j0 j1) = (j0,j1).
Proof with auto.
  induction b0; simpl; intros; destruct j0...
  + rewrite (IHb0 d j1)...
Qed.

Lemma dom_append_split {r0 r1 : nat} {b0 : NVect r0} {b1 : NVect r1} :
  forall (j : DomainT (b0 ++ b1)) (j0 : DomainT b0) (j1 : DomainT b1),
    (j0,j1) = split r0 j -> dom_append j0 j1 = j.
Proof with auto.
  induction b0; simpl; intros j j0 j1 Heq.
  + inversion Heq...
  + destruct j, j0, (split n d) eqn:Hs.
      inversion Heq; subst.
      rewrite (IHb0 d d1 d2 (eq_sym Hs))...
Qed.

(* Bijections between domains are useful for defining
   transpositions of tensors. More generally, bijections
   can define tensor operations that are usually referred
   to as 'reshape' or 'view':                             *)

Section Bijections.
  Variable r : nat.

  Record bijection (b0 b1 : NVect r) : Set := Bijection {
    f : DomainT b0 -> DomainT b1;
    g : DomainT b1 -> DomainT b0;

    id_gf : forall (i0 : DomainT b0), g (f i0) = i0;
    id_fg : forall (i1 : DomainT b1), f (g i1) = i1
  }.

  Arguments f {b0 b1}.
  Arguments g {b0 b1}.
  Arguments id_gf {b0 b1}.
  Arguments id_fg {b0 b1}.

  Lemma id_dom_UIP_dec {b : NVect r}
                       {h : DomainT b -> DomainT b} :
    forall (pf1 pf2 : forall (x : DomainT b), h x = x),
      pf1 = pf2.
  Proof.
    intros pf1 pf2.
    apply functional_extensionality_dep.
    intro x.
    apply (UIP_dec dom_eq_dec).
  Qed.

  Lemma id_gf_UIP_dec {b0 b1 : NVect r}
                      (f : DomainT b0 -> DomainT b1)
                      (g : DomainT b1 -> DomainT b0):
    forall (pf1 pf2 : forall (x : DomainT b0), g (f x) = x),
      pf1 = pf2.
  Proof.
    apply id_dom_UIP_dec.
  Qed.

  Lemma bij_equal {b0 b1 : NVect r}
                  (bij_1 bij_2 : bijection b0 b1) :
    f bij_1 = f bij_2 -> g bij_1 = g bij_2 ->
      bij_1 = bij_2.
  Proof with auto.
    destruct bij_1, bij_2; simpl; intros Hfeq Hgeq; subst.
    rewrite (id_gf_UIP_dec _ _ id_gf0 id_gf1);
      rewrite (id_gf_UIP_dec _ _ id_fg0 id_fg1)...
  Qed.

  Lemma bij_equal' {b0 b1 : NVect r}
                   (bij_1 bij_2 : bijection b0 b1) :
    (forall x, f bij_1 x = f bij_2 x) ->
      (forall y, g bij_1 y = g bij_2 y) ->
        bij_1 = bij_2.
  Proof with auto.
    intros; apply bij_equal; apply functional_extensionality...
  Qed.

  Definition compose {b0 b1 b2 : NVect r}
                     (bij_2 : bijection b1 b2)
                     (bij_1 : bijection b0 b1) : bijection b0 b2.
    refine({| f := Basics.compose (f bij_2) (f bij_1);
              g := Basics.compose (g bij_1) (g bij_2);
              id_gf := _;
              id_fg := _  |}).
  Proof with auto.
    + intro i0; unfold compose.
      rewrite (id_gf bij_2); rewrite (id_gf bij_1)...
    + intro i1; unfold compose.
      rewrite (id_fg bij_1); rewrite (id_fg bij_2)...
  Defined.

  Definition bij_inverse {b0 b1 : NVect r}
                         (bij : bijection b0 b1) : bijection b1 b0 :=
    {| f := g bij;
       g := f bij;
       id_gf := id_fg bij;
       id_fg := id_gf bij  |}.

  Definition identity {b : NVect r} : bijection b b :=
    {| f := id;
       g := id;
       id_gf := fun _ => eq_refl;
       id_fg := fun _ => eq_refl  |}.

  Lemma inverse_correct_1 {b : NVect r} (bij : bijection b b) :
    compose (bij_inverse bij) bij = identity.
  Proof with auto.
    apply bij_equal'; simpl; intro x; unfold Basics.compose;
      rewrite (id_gf bij)...
  Qed.

  Lemma inverse_correct_2 {b : NVect r} (bij : bijection b b) :
    compose bij (bij_inverse bij) = identity.
  Proof with auto.
    apply bij_equal'; simpl; intro x; unfold Basics.compose;
      rewrite (id_fg bij)...
  Qed.
End Bijections.

Arguments bijection {r}.
Arguments Bijection {r b0 b1}.
Arguments f {r b0 b1}.
Arguments g {r b0 b1}.
Arguments id_gf {r b0 b1}.
Arguments id_fg {r b0 b1}.

(* Transposition of the first two elements in a tuple: *)

Definition f_01 {r : nat} {b0 b1 : nat} {bnds : NVect r} :
  DomainT (b0::b1::bnds) -> DomainT (b1::b0::bnds) :=
  fun i => let (i0,i')  := i in
           let (i1,i'') := i' in
           (i1,(i0,i'')).

Lemma f_01_self_inverse {r : nat} {b0 b1 : nat} {bnds : NVect r} :
  forall (i : DomainT (b0::b1::bnds)), f_01 (f_01 i) = i.
Proof.
  destruct i as [i0 i'].
  destruct i' as [i1 i''].
  reflexivity.
Qed.

Definition transp_01 {r : nat} (b0 b1 : nat) (bnds : NVect r) :=
  {| f := @f_01 r b0 b1 bnds;
     g := @f_01 r b1 b0 bnds;
     id_gf := f_01_self_inverse;
     id_fg := f_01_self_inverse  |}.

author: normanrink

repo: TensorIR

save_path: github-repos/coq/normanrink-TensorIR