text:
(* begin hide *)

From mathcomp Require Import all_ssreflect.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

From Equations Require Import Equations.

Require Import String.
Require Import QString.

Require Import Value.

Require Import Schema.
Require Import SchemaAux.
Require Import SchemaWellFormedness.

Require Import Query.

Require Import SeqExtra.

Require Import Ssromega.

(* end hide *)

(**
   #

GraphQL Query Auxiliary

         This file contains auxiliary definitions used with a GraphQL Query.

         Some of these are: query size, extractors for selections, general purpose predicates, etc.

#
 *)

Section QueryAux.

  Variable (Scalar : eqType).

  Implicit Type σs : seq (@Selection Scalar).
  Implicit Type σ : @Selection Scalar.

  (** *** General purpose predicates *)
  (** ---- *)
  Section Base.

    (**
        Checks whether the given selection is a field selection.
     *)
    Equations is_field σ : bool :=
      {
        is_field (on _ { _ }) := false;
        is_field _ := true
      }.

    (** ---- *)
    (**
       Checks whether the given selection is an inline fragment.
     *)
    Equations is_inline_fragment σ : bool :=
      {
        is_inline_fragment (on _ { _ }) := true;
        is_inline_fragment _ := false
      }.

    (** *** Extractors for selections *)
    (** ---- *)

    (**
       Gets the name of the given selection.

       Inline fragments do not have a name, therefore
       it is required that the given selection is a field.
     *)
    Equations qname σ (Hfield : σ.(is_field)) : Name :=
      {
        qname (name[[ _ ]]) _ := name;
        qname (_:name[[ _ ]]) _ := name;
        qname (name[[ _ ]] { _ }) _ := name;
        qname (_:name[[ _ ]] { _ }) _ := name;
        qname (on _ { _ }) Hfld := _
      }.
    (**
       Gets the response name of the given selection.

       For aliased fields this corresponds to their alias, while for
       non-aliased fields it corresponds to their name.

       Inline fragment do not have a response name, therefore
       it is required that the given selection is a field.
     *)
    Equations qresponse_name σ (Hfld : σ.(is_field)) :  Name :=
      {
        qresponse_name (name [[ _ ]]) _ := name;
        qresponse_name (alias : _ [[ _ ]]) _ := alias;
        qresponse_name (name [[ _ ]] { _ }) _ := name;
        qresponse_name (alias : _ [[ _ ]] { _ }) _ := alias;
        qresponse_name (on _ { _ }) Hfld := _
      }.

    (** ---- *)
    (**
       Gets the given selection's subselections.

       For field selections without subselections, it returns an empty list.
     *)
    Definition subselections σ : seq Selection :=
      match σ with
      | _ [[ _ ]] { φ }
      | _ : _ [[ _ ]] { φ }
      | on _ { φ } => φ
      | _ => [::]
      end.

    (** ---- *)
    (**
       Gets the given selection's arguments.

       Inline fragment do not have arguments, therefore
       it is required that the given selection is a field.
     *)
    Equations qargs σ (Hfld : σ.(is_field)) :  seq (Name * @Value Scalar) :=
      {
        qargs (_ [[ α ]]) _ := α;
        qargs (_ : _ [[ α ]]) _ := α;
        qargs (_ [[ α ]] { _ }) _ := α;
        qargs (_ : _ [[ α ]] { _ }) _ := α;
        qargs (on _ { _ }) Hfld := _
      }.

    (** ---- *)
    (**
       Checks whether two selections have the same field name.

       It is always false if either is an inline fragment.
     *)
    Equations have_same_name : @Selection Scalar -> @Selection Scalar -> bool :=
      {
        have_same_name (on _ { _ }) _ := false;
        have_same_name _ (on _ { _ }) := false;
        have_same_name σ1 σ2 := (qname σ1 _) == (qname σ2 _)
      }.

    (** ---- *)
    (**
       Checks whether two selections have the same arguments.

       It is always false if either is an inline fragment.
     *)
    Equations have_same_arguments : @Selection Scalar -> @Selection Scalar -> bool :=
      {
        have_same_arguments (on _ { _ }) _ := false;
        have_same_arguments _ (on _ { _ }) := false;
        have_same_arguments σ1 σ2 := (qargs σ1 _) == (qargs σ2 _)
      }.

    (** ---- *)
    (**
       Checks whether the given selection is either a [SingleField] or [SingleAliasedField].
     *)
    Equations is_simple_field_selection σ : bool :=
      {
        is_simple_field_selection (_ [[_]]) := true;
        is_simple_field_selection (_ : _ [[_]]) := true;
        is_simple_field_selection _ := false
      }.

    (** ---- *)
    (**
       Checks whether the given selection is either a [NestedField] or [NestedAliasedField].
     *)
    Equations is_nested_field_selection σ : bool :=
      {
        is_nested_field_selection (_ [[_]] { _ }) := true;
        is_nested_field_selection (_ : _ [[_]] { _ }) := true;
        is_nested_field_selection _ := false
      }.

    (** ---- *)
    (**
       Decides whether two selections are equal, considering possible permutation
       of arguments in field selections.
     *)
    Equations selection_perm_eq (σ1 σ2 : @Selection Scalar) : bool :=
      {
        selection_perm_eq (f1[[α1]]) (f2[[α2]]) := (f1 == f2) && perm_eq α1 α2;
        selection_perm_eq (a1:f1[[α1]]) (a2:f2[[α2]]) := [&& a1 == a2, f1 == f2 & perm_eq α1 α2];
        selection_perm_eq (f1[[α1]] { σs1 }) (f2[[α2]] { σs2 }) :=
          [&& f1 == f2, perm_eq α1 α2 & selections_perm_eq σs1 σs2];
        selection_perm_eq (a1:f1[[α1]] { σs1 }) (a2:f2[[α2]] { σs2 }) :=
          [&& a1 == a2, f1 == f2, perm_eq α1 α2 & selections_perm_eq σs1 σs2];
        selection_perm_eq (on t1 { σs1 }) (on t2 { σs2 }) :=
          (t1 == t2) && (selections_perm_eq σs1 σs2);
        selection_perm_eq _ _ := false
      }
    where selections_perm_eq (σs1 σs2 : seq (@Selection Scalar)) : bool :=
            {
              selections_perm_eq [::] [::] := true;
              selections_perm_eq (σ1 :: σs1) (σ2 :: σs2) := selection_perm_eq σ1 σ2 && selections_perm_eq σs1 σs2;
              selections_perm_eq _ _ := false
            }.

    (** ---- *)
    (**
       Checks whether two selections are equivalent.

       This equivalence refers to whether both selections will
       produce responses with the same name and if both
       share the same arguments.

       **** See also
       - [is_field_merging_possible]
     *)
    (* FIXME : Rename *)
    Definition are_equivalent (σ1 σ2 : @Selection Scalar) : bool :=
      [&& (σ1.(is_simple_field_selection) && (σ2.(is_simple_field_selection)) ||
           σ1.(is_nested_field_selection) && σ2.(is_nested_field_selection)),
       have_same_name σ1 σ2 & have_same_arguments σ1 σ2].

  End Base.

  (** *** Size functions
      ----

      In this section we define functions related to
      the size of queries.
   *)
  Section Size.

    (**
       Get the size of a selection and selection set, according to H&P's definition.
     *)
    Equations selection_size σ : nat :=
      {
        selection_size (_ [[_]] { σs }) := 1 + selections_size σs;
        selection_size (_ : _ [[_]] { σs }) := 1 + selections_size σs;
        selection_size (on _ { σs }) := 1 + (selections_size σs);
        selection_size _ := 1
      }
    where
    selections_size σs : nat :=
      {
        selections_size [::] := 0;
        selections_size (σ :: σs) := selection_size σ + selections_size σs
      }.

    (** ---- *)
    (**
       Get the size of a selection set paired with its type in scope.
     *)
    Definition selections_size_aux (scoped_σs : seq (Name * Selection)) :=
      selections_size [seq sσ.2 | sσ <- scoped_σs].

    (** ---- *)
    (**
       Get the size of a query.
     *)
    Definition query_size (φ : @query Scalar) :=
      selections_size φ.(selection_set).

  End Size.

  (** *** Other type of predicates *)
  (** ---- *)

  Section DefPreds.

    Variable s : wfGraphQLSchema.

    (**
       This predicate checks whether a type condition is valid in
       a given object type and is necessary to check if a fragment must be evaluated.

       This definition is similar to the one in the spec
       (cf. #§6.3.2#).
       The difference is simply to facilitate reasoning over it.
     *)
    Definition does_fragment_type_apply object_type fragment_type :=
      match lookup_type s object_type, lookup_type s fragment_type with
      | Some (object oname implements _ { _ }), Some (object name implements _ { _ }) =>
        object_type == name
      | Some (object _ implements interfaces { _ }), Some (interface name { _ }) =>
        name \in interfaces
      | Some (object oname implements _ { _ }), Some (union name { members }) =>
        oname \in members
      | _, _ => false
      end.

    (** ---- *)
    (**
     Checks whether a given type can be used as an inline fragment's type condition
     in a given context with another type in scope
     (cf. #§5.5.2.3#).

     It basically amounts to intersecting the possible subtypes of each
     and checking that the intersection is not empty.
     *)
    (* The definition of seqI is a bit annoying, maybe we could change it to
       has (fun ty => ty \in parent_possible_types) ty_possible_types, which is
       much simpler to reason about *)
    Definition is_fragment_spread_possible parent_type fragment_type : bool :=
      let ty_possible_types := get_possible_types s fragment_type in
      let parent_possible_types := get_possible_types s parent_type in
      let applicable_types := (ty_possible_types :&: parent_possible_types)%SEQ in
      applicable_types != [::].

  End DefPreds.

  (** *** Functions related to finding selections that satisfy a predicate *)
  (** ---- *)
  Section Find.

    Variable (s : wfGraphQLSchema).

    (**
       Find selections with response name equal to a given name.
       In case there is a fragment, it first checks that the fragment's type condition
       applies to the given object type, then it may proceed finding in its subselections.

     *)
    Equations? find_valid_fields_with_response_name (label : Name) (object_type : Name) (σs : seq (@Selection Scalar)) :
      seq (@Selection Scalar) by wf (selections_size σs) :=
      {
        find_valid_fields_with_response_name _ _ [::] := [::];

        find_valid_fields_with_response_name k O__t (on t { βs } :: σs)
          with does_fragment_type_apply s O__t t :=
          {
          | true := find_valid_fields_with_response_name k O__t βs ++ find_valid_fields_with_response_name k O__t σs;
          | _ := find_valid_fields_with_response_name k O__t σs
          };

        find_valid_fields_with_response_name k O__t (σ :: σs)
          with (qresponse_name σ _) == k :=
          {
          | true := σ :: find_valid_fields_with_response_name k O__t σs;
          | _ := find_valid_fields_with_response_name k O__t σs
          }
      }.
    all: do ?simp selection_size; ssromega.
    Qed.

    (** ---- *)
    (**
       Find selections with response name equal to a given name.
       In case there is a fragment, it first checks that the fragment's type condition
       applies to the given object type, then it may proceed finding in its subselections.

     *)
    Equations? find_valid_pairs_with_response_name (ts : Name) (rname : Name) (σs : seq (Name * @Selection Scalar)) :
      seq (Name * @Selection Scalar) by wf (selections_size_aux σs) :=
      {
        find_valid_pairs_with_response_name _ _ [::] := [::];

        find_valid_pairs_with_response_name ts rname ((_, on t { βs }) :: σs)
          with does_fragment_type_apply s ts t :=
          {
          | true := find_valid_pairs_with_response_name rname ts [seq (t, β) | β <- βs] ++ find_valid_pairs_with_response_name ts rname σs;
          | _ := find_valid_pairs_with_response_name ts rname σs
          };

        find_valid_pairs_with_response_name ts rname ((t, σ) :: σs)
          with (qresponse_name σ _) == rname :=
          {
          | true := (t, σ) :: find_valid_pairs_with_response_name rname ts σs;
          | _ := find_valid_pairs_with_response_name rname ts σs
          }
      }.
    all: do ? [rewrite /selections_size_aux /=; simp selection_size; rewrite -/(selections_size_aux _); ssromega].
      by rewrite /selections_size_aux /=; simp selection_size; rewrite -map_comp /funcomp /= map_id; ssromega.
    Qed.

    (** ---- *)
    (**
        Find all selections with response name equal to a given name.
        It collects every field, regardless of fragment's type condition. This differs
        with [find_valid_fields_with_response_name], where the type condition _is_ important.
     *)
    (* FIXME : Rename considering previous def *)
    Equations? find_fields_with_response_name (rname : Name) (σs : seq (@Selection Scalar)) :
      seq (@Selection Scalar) by wf (selections_size σs) :=
      {
        find_fields_with_response_name _ [::] := [::];

        find_fields_with_response_name rname (f [[α]] :: σs)
          with f == rname :=
          {
          | true := f [[α]] :: find_fields_with_response_name rname σs;
          | _ := find_fields_with_response_name rname σs
          };

        find_fields_with_response_name rname (l : f [[α]] :: σs)
          with l == rname :=
          {
          | true := l : f [[α]] :: find_fields_with_response_name rname σs;
          | _ := find_fields_with_response_name rname σs
          };

        find_fields_with_response_name rname (f [[α]] { βs } :: σs)
          with f == rname :=
          {
          | true := f [[α]] { βs } :: find_fields_with_response_name rname σs;
          | _ := find_fields_with_response_name rname σs
          };

        find_fields_with_response_name rname (l : f [[α]] { βs }:: σs)
          with l == rname :=
          {
          | true := l : f [[α]] { βs } :: find_fields_with_response_name rname σs;
          | _ := find_fields_with_response_name rname σs
          };

        find_fields_with_response_name rname (on t { βs } :: σs) :=
          find_fields_with_response_name rname βs ++ find_fields_with_response_name rname σs
      }.
    Proof.
      all: do [by simp selection_size; ssromega].
    Qed.

    (** ---- *)
    (**
        Find all selections with response name equal to a given name.
        It collects every field, regardless of fragment's type condition. This differs
        with [find_valid_fields_with_response_name], where the type condition _is_ important.

     *)
    Equations? find_pairs_with_response_name (rname : Name) (σs : seq (Name * @Selection Scalar)) :
      seq (Name * @Selection Scalar) by wf (selections_size_aux σs) :=
      {
        find_pairs_with_response_name _ [::] := [::];

        find_pairs_with_response_name rname ((ty, f[[α]]) :: σs)
          with f == rname :=
          {
          | true := (ty, f[[α]]) :: find_pairs_with_response_name rname σs;
          | _ := find_pairs_with_response_name rname σs
          };

        find_pairs_with_response_name rname ((ty, l:f[[α]]) :: σs)
          with l == rname :=
          {
          | true := (ty, l:f[[α]]) :: find_pairs_with_response_name rname σs;
          | _ := find_pairs_with_response_name rname σs
          };

        find_pairs_with_response_name rname ((ty, f[[α]] { βs }) :: σs)
          with f == rname :=
          {
          | true := (ty, f[[α]] { βs }) :: find_pairs_with_response_name rname σs;
          | _ := find_pairs_with_response_name rname σs
          };

        find_pairs_with_response_name rname ((ty, l:f[[α]] { βs }) :: σs)
          with l == rname :=
          {
          | true := (ty, l:f[[α]] { βs }) :: find_pairs_with_response_name rname σs;
          | _ := find_pairs_with_response_name rname σs
          };

        find_pairs_with_response_name rname ((_, on t { βs }) :: σs) :=
          find_pairs_with_response_name rname [seq (t, q) | q <- βs] ++ find_pairs_with_response_name rname σs
      }.
    Proof.
      all: do ? [by rewrite /selections_size_aux /=; simp selection_size; ssromega].
      rewrite /selections_size_aux /=; simp selection_size.
      have -> : forall xs y, [seq x.2 | x <- [seq (y, q) | q <- xs] ] = xs.
        by intros; elim: xs => //= x xs ->.
        by ssromega.
    Qed.

    (** ---- *)
    (**
       Find all fragments with type condition equal to a given type.
     *)
    Equations find_fragment_with_type_condition : Name -> seq (@Selection Scalar) -> seq (@Selection Scalar) :=
      {
        find_fragment_with_type_condition _ [::] := [::];

        find_fragment_with_type_condition t (on t' { β } :: σs)
          with t == t' :=
          {
          | true := on t { β } :: find_fragment_with_type_condition t σs;
          | _ := find_fragment_with_type_condition t σs
          };

        find_fragment_with_type_condition t (σ :: σs) := find_fragment_with_type_condition t σs
      }.

  End Find.

  (** *** Functions related to filtering queries according to some predicate *)
  (** ---- *)
  Section Filter.

    (**
        Remove all fields with a given response name.
     *)
    Equations? filter_fields_with_response_name (label : Name) (σs : seq (@Selection Scalar)) :
      seq (@Selection Scalar) by wf (selections_size σs) :=
      {
        filter_fields_with_response_name _ [::] := [::];

        filter_fields_with_response_name l (on t { β } :: σs) :=
          on t { filter_fields_with_response_name l β } :: filter_fields_with_response_name l σs;

        filter_fields_with_response_name l (σ :: σs)
          with (qresponse_name σ _) != l :=
          {
          | true := σ :: filter_fields_with_response_name l σs;
          | _ := filter_fields_with_response_name l σs
          }

      }.
    all: do ?[simp selection_size; ssromega].
    Qed.

    (** ---- *)
    (**
       Remove all fields with a given response name.
     *)
     Equations? filter_pairs_with_response_name (response_name : Name) (σs : seq (Name * @Selection Scalar)) :
      seq (Name * @Selection Scalar) by wf (selections_size_aux σs) :=
      {
        filter_pairs_with_response_name _ [::] := [::];

        filter_pairs_with_response_name l ((ty, on t { β }) :: σs) :=
          (ty, on t { filter_fields_with_response_name l β }) :: filter_pairs_with_response_name l σs;

        filter_pairs_with_response_name l ((ty, σ) :: σs)
          with (qresponse_name σ _) != l :=
          {
          | true := (ty, σ) :: filter_pairs_with_response_name l σs;
          | _ := filter_pairs_with_response_name l σs
          }

      }.
     Proof.
       all: do ? [by rewrite /selections_size_aux /=; simp selection_size; ssromega].
    Qed.

  End Filter.

  (** *** Functions related to merging queries *)
  (** ---- *)
  Section Merging.

    (**
       Concatenates the subqueries of every selection in the given list.
     *)
    Definition merge_selection_sets σs := flatten [seq σ.(subselections) | σ <- σs].

    Variable (s : wfGraphQLSchema).

    (** ---- *)
    (**
       Concatenates the subqueries of every selection in the given list.
     *)
    Equations merge_pairs_selection_sets (scoped_σs : seq (Name * @Selection Scalar)) : seq (Name * @Selection Scalar) :=
      {
        merge_pairs_selection_sets [::] := [::];

        merge_pairs_selection_sets ((ty, f[[ _ ]] { βs }) :: σs)
          with lookup_field_in_type s ty f :=
          {
          | Some fld := [seq (fld.(ftype).(tname), σ) | σ <- βs] ++ merge_pairs_selection_sets σs;
          | _ := merge_pairs_selection_sets σs
          };

        merge_pairs_selection_sets ((ty, _:f[[ _ ]] { βs }) :: σs)
          with lookup_field_in_type s ty f :=
          {
          | Some fld := [seq (fld.(ftype).(tname), σ) | σ <- βs] ++ merge_pairs_selection_sets σs;
          | _ := merge_pairs_selection_sets σs
          };

        merge_pairs_selection_sets ((_, on t { βs }) :: σs) :=
          [seq (t, σ) | σ <- βs] ++ merge_pairs_selection_sets σs;

        merge_pairs_selection_sets (scoped_σs :: σs) := merge_pairs_selection_sets σs
      }.

  End Merging.

End QueryAux.

(** ---- *)

(**
    #

         Previous ← Query
        Next → Query Conformance

#
 *)

(** ---- *)

(* begin hide *)
Arguments is_field [Scalar].
Arguments is_inline_fragment [Scalar].

Arguments is_simple_field_selection [Scalar].
Arguments is_nested_field_selection [Scalar].

Arguments qname [Scalar].
Arguments qargs [Scalar].

Arguments subselections [Scalar].
Arguments qresponse_name [Scalar].

Arguments selection_size [Scalar].
Arguments selections_size [Scalar].
Arguments selections_size_aux [Scalar].
Arguments query_size [Scalar].

Arguments have_same_name [Scalar].
Arguments have_same_arguments [Scalar].
Arguments are_equivalent [Scalar].

Arguments filter_fields_with_response_name [Scalar].
Arguments filter_pairs_with_response_name [Scalar].

Arguments find_valid_fields_with_response_name [Scalar].
Arguments find_valid_pairs_with_response_name [Scalar].
Arguments find_fields_with_response_name [Scalar].
Arguments find_pairs_with_response_name [Scalar].
Arguments find_fragment_with_type_condition [Scalar].

Arguments merge_selection_sets [Scalar].
Arguments merge_pairs_selection_sets [Scalar].

(* end hide *)

author: imfd

repo: GraphCoQL

save_path: github-repos/coq/imfd-GraphCoQL


(* This file contains lemmas regarding the accuracy of floating point
  operations such as BPLUS, BFMA, and BMULT. *)

Require Import vcfloat.VCFloat.
Require Import common op_defs.

Section GenFloat.
Context {t : type}.

Lemma Bmult_0R {NAN: Nans} a f :
Binary.is_finite (fprec t) (femax t) (BMULT a f) = true ->
FT2R a = 0 ->
(BMULT a f) = neg_zero \/ (BMULT a f) = pos_zero.
Proof. intros; destruct f; destruct a; simpl; try discriminate;
destruct s; destruct s0; simpl; auto;
unfold FT2R, Binary.B2R in H0; simpl in H0;
apply Float_prop.eq_0_F2R in H0;
discriminate.
Qed.

Lemma Bplus_0R {NAN: Nans} a f :
Binary.is_finite (fprec t) (femax t) (BPLUS a f) = true ->
FT2R f = 0 ->
FT2R (BPLUS a f) = FT2R a.
Proof.
intros; destruct f; destruct a; simpl; try discriminate;
destruct s; destruct s0; simpl; auto;
unfold FT2R, Binary.B2R in H0; simpl in H0;
apply Float_prop.eq_0_F2R in H0;
discriminate.
Qed.

Lemma Bfma_mult_0R {NAN: Nans} a f s :
Binary.is_finite (fprec t) (femax t) (BFMA a f s) = true ->
FT2R a = 0 ->
FT2R (BFMA a f s) = FT2R s.
Proof. intros; destruct f; destruct a; destruct s; simpl; try discriminate;
destruct s; destruct s0; destruct s1; simpl; auto;
unfold FT2R, Binary.B2R in H0; simpl in H0;
apply Float_prop.eq_0_F2R in H0;
discriminate.
Qed.

Lemma neg_zero_is_finite:
Binary.is_finite (fprec t) (femax t) neg_zero = true.
Proof. simpl; auto. Qed.

Definition fma_no_overflow (x y z: R) : Prop :=
  (Rabs (rounded t  (x * y + z)) < Raux.bpow Zaux.radix2 (femax t))%R.

Definition Bmult_no_overflow (x y: R) : Prop :=
  (Rabs (rounded t  (x * y)) < Raux.bpow Zaux.radix2 (femax t))%R.

Notation D := (@default_rel t).
Notation E := (@default_abs t).

Lemma generic_round_property:
  forall (x: R),
exists delta epsilon : R,
   delta * epsilon = 0 /\
  (Rabs delta <= D)%R /\
  (Rabs epsilon <= E)%R /\
   Generic_fmt.round Zaux.radix2
              (SpecFloat.fexp (fprec t) (femax t))
              (BinarySingleNaN.round_mode BinarySingleNaN.mode_NE)
               x = (x * (1+delta)+epsilon)%R.
Proof.
intros.
destruct (Relative.error_N_FLT Zaux.radix2 (SpecFloat.emin (fprec t) (femax t)) (fprec t)
             (fprec_gt_0 t) (fun x0 : Z => negb (Z.even x0)) x)
  as [delta [epsilon [? [? [? ?]]]]].
exists delta, epsilon.
repeat split; auto.
Qed.

Lemma fma_accurate {NAN: Nans} :
   forall x (FINx: Binary.is_finite (fprec t) (femax t) x = true)
          y (FINy: Binary.is_finite (fprec t) (femax t) y = true)
          z (FINz: Binary.is_finite (fprec t) (femax t) z = true)
          (FIN: fma_no_overflow (FT2R x) (FT2R y) (FT2R z)),
  exists delta, exists epsilon,
   delta * epsilon = 0 /\
   Rabs delta <= D /\
   Rabs epsilon <= E /\
   (FT2R (BFMA x y z) = (FT2R x * FT2R y + FT2R z) * (1+delta) + epsilon)%R.
Proof.
intros.
pose proof (Binary.Bfma_correct  (fprec t) (femax t)  (fprec_gt_0 t) (fprec_lt_femax t) (fma_nan t)
                      BinarySingleNaN.mode_NE x y z FINx FINy FINz).
change (Binary.B2R (fprec t) (femax t) ?x) with (@FT2R t x) in *.
cbv zeta in H.
pose proof (
   Raux.Rlt_bool_spec
        (Rabs
           (Generic_fmt.round Zaux.radix2
              (SpecFloat.fexp (fprec t) (femax t))
              (BinarySingleNaN.round_mode
                 BinarySingleNaN.mode_NE) (FT2R x * FT2R y + FT2R z)))
        (Raux.bpow Zaux.radix2 (femax t))).
destruct H0.
-
destruct H as [? _].
fold (@BFMA NAN t) in H.
rewrite H.
apply generic_round_property.
-
red in FIN. unfold rounded in FIN.
Lra.lra.
Qed.

Lemma is_finite_fma_no_overflow {NAN: Nans}:
  forall x y z
  (HFINb : Binary.is_finite (fprec t) (femax t) (BFMA x y z) = true),
  fma_no_overflow (FT2R x) (FT2R y) (FT2R z).
Proof.
intros.
red. set (ov:= bpow Zaux.radix2 (femax t)).
pose proof Rle_or_lt ov (Rabs (rounded t (FT2R x * FT2R y + FT2R z)))  as Hor;
  destruct Hor; auto.
apply Rlt_bool_false in H.
assert (HFIN: Binary.is_finite (fprec t) (femax t) x = true /\
  Binary.is_finite (fprec t) (femax t) y = true /\
  Binary.is_finite (fprec t) (femax t) z = true).
{ unfold BFMA in HFINb.
    destruct x; destruct y; destruct z; simpl in *; try discriminate; auto.
    all: destruct s; destruct s0; destruct s1; simpl in *; try discriminate; auto. }
destruct HFIN as (A & B & C).
unfold rounded, FT2R, ov in H.
pose proof (Binary.Bfma_correct  (fprec t) (femax t)
    (fprec_gt_0 t) (fprec_lt_femax t) (fma_nan t) BinarySingleNaN.mode_NE x y z A B C) as
  H0.
simpl in H0; simpl in H;
rewrite H in H0. clear H. fold (@BFMA NAN t) in H0.
destruct (BFMA x y z); try discriminate.
Qed.

Lemma fma_accurate' {NAN: Nans} :
   forall (x y z : ftype t)
          (FIN: Binary.is_finite _ _ (BFMA x y z) = true),
  exists delta, exists epsilon,
   delta * epsilon = 0 /\
   Rabs delta <= D /\
   Rabs epsilon <= E /\
   (FT2R (BFMA x y z) = (FT2R x * FT2R y + FT2R z) * (1+delta) + epsilon)%R.
Proof.
intros.
assert (FIN2: Binary.is_finite (fprec t) (femax t) x = true /\
        Binary.is_finite (fprec t) (femax t) y = true /\
        Binary.is_finite (fprec t) (femax t) z = true).
destruct x; destruct y; destruct z; simpl in *; try discriminate; auto;
destruct s; destruct s0; destruct s1; try discriminate; auto.
destruct FIN2 as (FINx & FINy & FINz).
apply fma_accurate; auto.
apply is_finite_fma_no_overflow; auto.
Qed.

Lemma BMFA_finite_e {NAN: Nans} :
 forall (a u f : ftype t)
 (Hfin : Binary.is_finite _ _ (BFMA a f u) = true),
 Binary.is_finite _ _ a = true  /\
 Binary.is_finite _ _ f = true /\
 Binary.is_finite _ _ u = true.
Proof.
intros.
destruct a,f,u; inversion Hfin; clear Hfin; subst;
 try solve [split; [ | split]; simpl; auto; constructor; auto].
all: try solve [destruct s,s0,s1; discriminate].
Qed.

Lemma BMULT_accurate {NAN: Nans}:
   forall  x y (FIN: Bmult_no_overflow  (FT2R x) (FT2R y)),
  exists delta, exists epsilon,
   delta * epsilon = 0 /\
   Rabs delta <= D /\
   Rabs epsilon <= E /\
   (@FT2R t (BMULT x y) = (FT2R x * FT2R y) * (1+delta) + epsilon)%R.
Proof.
intros.
pose proof (Binary.Bmult_correct (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t)
                (mult_nan t) BinarySingleNaN.mode_NE x y).
change (Binary.B2R (fprec t) (femax t) ?x) with (@FT2R t x) in *.
cbv zeta in H.
pose proof (
   Raux.Rlt_bool_spec
        (Rabs
           (Generic_fmt.round Zaux.radix2
              (SpecFloat.fexp (fprec t) (femax t))
              (BinarySingleNaN.round_mode
                 BinarySingleNaN.mode_NE) (FT2R x * FT2R y)))
        (Raux.bpow Zaux.radix2 (femax t))).
destruct H0.
destruct H as [? _].
unfold BMULT, BINOP.
rewrite H.
apply generic_round_property.
red in FIN. unfold rounded in FIN.
Lra.lra.
Qed.

Lemma is_finite_BMULT_no_overflow {NAN: Nans} :
  forall (x y : ftype t)
  (HFINb : Binary.is_finite (fprec t) (femax t) (BMULT x y) = true),
  Bmult_no_overflow  (FT2R x) (FT2R y).
Proof.
intros.
pose proof Rle_or_lt (bpow Zaux.radix2 (femax t))
  (Rabs (rounded t (FT2R x * FT2R y)))  as Hor;
  destruct Hor; auto.
apply Rlt_bool_false in H; red.
unfold rounded, FT2R  in H.
pose proof (Binary.Bmult_correct  (fprec t) (femax t)
    (fprec_gt_0 t) (fprec_lt_femax t) (mult_nan t) BinarySingleNaN.mode_NE x y) as
  H0.
simpl in H0; simpl in H;
rewrite H in H0.  unfold BMULT, BINOP in HFINb.
destruct ((Binary.Bmult (fprec t) (femax t) (fprec_gt_0 t)
             (fprec_lt_femax t) (mult_nan t) BinarySingleNaN.mode_NE x y));
simpl;  try discriminate.
Qed.

Lemma BMULT_accurate' {NAN: Nans}:
  forall
  (x y : ftype t)
  (FIN: Binary.is_finite _ _ (BMULT x y) = true),
  exists delta, exists epsilon,
   delta * epsilon = 0 /\
   Rabs delta <= D /\
   Rabs epsilon <= E /\
   (@FT2R t (BMULT x y) = (FT2R x * FT2R y) * (1+delta) + epsilon)%R.
Proof.
intros.
pose proof BMULT_accurate  x y (is_finite_BMULT_no_overflow x y FIN); auto.
Qed.

Lemma BMULT_finite_e {NAN: Nans} :
 forall (a b : ftype t)
 (Hfin : Binary.is_finite _ _ (BMULT a b) = true),
 Binary.is_finite _ _ a = true  /\
 Binary.is_finite _ _ b = true.
Proof.
intros.
destruct a,b; inversion Hfin; clear Hfin; subst; auto.
Qed.

Lemma BPLUS_finite_e {NAN: Nans}:
 forall (a b : ftype t)
 (Hfin : Binary.is_finite _ _ (BPLUS a b) = true),
 Binary.is_finite _ _ a = true  /\
 Binary.is_finite _ _ b = true.
Proof.
intros.
destruct a,b; inversion Hfin; clear Hfin; subst; simpl; auto.
destruct s,s0; discriminate; auto.
Qed.

Definition Bplus_no_overflow (t: type) (x y: R) : Prop :=
  (Rabs ( Generic_fmt.round Zaux.radix2
              (SpecFloat.fexp (fprec t) (femax t))
              (BinarySingleNaN.round_mode
                 BinarySingleNaN.mode_NE)  (x + y )) < Raux.bpow Zaux.radix2 (femax t))%R.

Lemma BPLUS_neg_zero {NAN: Nans} (a : ftype t) :
  Binary.is_finite _ _ a = true ->
  BPLUS a neg_zero = a.
Proof.
destruct a; unfold neg_zero; simpl; try discriminate; auto.
destruct s; auto.
Qed.

Lemma BPLUS_B2R_zero {NAN: Nans}  (a : ftype t) :
  Binary.is_finite _ _ a = true ->
  FT2R (BPLUS a (Zconst t 0)) = FT2R a.
Proof.
destruct a; unfold neg_zero; simpl; try discriminate; auto.
destruct s; auto.
Qed.

Lemma BPLUS_accurate {NAN: Nans} :
 forall      x (FINx: Binary.is_finite (fprec t) (femax t) x = true)
             y (FINy: Binary.is_finite (fprec t) (femax t) y = true)
          (FIN: Bplus_no_overflow t (FT2R x) (FT2R y)),
  exists delta,
   Rabs delta <= D /\
   (FT2R (BPLUS x y ) = (FT2R x + FT2R y) * (1+delta))%R.
Proof.
intros.
pose proof (Binary.Bplus_correct  (fprec t) (femax t)  (fprec_gt_0 t) (fprec_lt_femax t) (plus_nan t)
                      BinarySingleNaN.mode_NE x y FINx FINy).
change (Binary.B2R (fprec t) (femax t) ?x) with (@FT2R t x) in *.
cbv zeta in H.
pose proof (
   Raux.Rlt_bool_spec
        (Rabs
           (Generic_fmt.round Zaux.radix2
              (SpecFloat.fexp (fprec t) (femax t))
              (BinarySingleNaN.round_mode
                 BinarySingleNaN.mode_NE) (FT2R x + FT2R y)))
        (Raux.bpow Zaux.radix2 (femax t))).
destruct H0.
-
destruct H as [? _].
unfold BPLUS, BINOP.
rewrite H.
assert (A: Generic_fmt.generic_format Zaux.radix2
       (FLT.FLT_exp (SpecFloat.emin (fprec t) (femax t)) (fprec t))
       (FT2R x) ) by (apply Binary.generic_format_B2R).
assert (B: Generic_fmt.generic_format Zaux.radix2
       (FLT.FLT_exp (SpecFloat.emin (fprec t) (femax t)) (fprec t))
       (FT2R y) ) by (apply Binary.generic_format_B2R).
pose proof Plus_error.FLT_plus_error_N_ex   Zaux.radix2 (SpecFloat.emin (fprec t) (femax t))
 (fprec t) (fun x0 : Z => negb (Z.even x0)) (FT2R x) (FT2R y) A B.
unfold Relative.u_ro in H1. fold (D) in H1.
destruct H1 as (d & Hd & Hd').
assert (  Generic_fmt.round Zaux.radix2 (SpecFloat.fexp (fprec t) (femax t))
    (BinarySingleNaN.round_mode BinarySingleNaN.mode_NE)
    (FT2R x + FT2R y)  =  Generic_fmt.round Zaux.radix2
        (FLT.FLT_exp (SpecFloat.emin (fprec t) (femax t)) (fprec t))
        (Generic_fmt.Znearest (fun x0 : Z => negb (Z.even x0)))
        (FT2R x + FT2R y)) by auto.
rewrite <- H1 in Hd'. clear H1. rewrite Hd'; clear Hd'.
exists d; split; auto.
eapply Rle_trans; [apply Hd |].
apply Rdiv_le_left.
apply Fourier_util.Rlt_zero_pos_plus1.
apply default_rel_gt_0.
eapply Rle_trans with (D * 1); try nra.
-
red in FIN.
Lra.lra.
Qed.

Lemma is_finite_sum_no_overflow {NAN: Nans}  :
  forall x y
  (HFINb : Binary.is_finite (fprec t) (femax t) (BPLUS x y) = true),
  Bplus_no_overflow t (FT2R x) (FT2R y).
Proof.
intros.
pose proof Rle_or_lt (bpow Zaux.radix2 (femax t)) (Rabs (rounded t (FT2R x + FT2R y)))  as Hor;
  destruct Hor; auto.
apply Rlt_bool_false in H.
assert (HFIN: Binary.is_finite (fprec t) (femax t) x = true /\
  Binary.is_finite (fprec t) (femax t) y = true).
{ unfold BPLUS, BINOP in HFINb.
    destruct x; destruct y; simpl in *; try discriminate; auto.
    destruct s; destruct s0; simpl in *; try discriminate; auto.
}
destruct HFIN as (A & B).
unfold rounded, FT2R in H.
pose proof (Binary.Bplus_correct  (fprec t) (femax t)
    (fprec_gt_0 t) (fprec_lt_femax t) (plus_nan t) BinarySingleNaN.mode_NE x y A B) as
  H0;
rewrite H in H0;
destruct H0 as ( C & _).
unfold BPLUS, BINOP in HFINb.
destruct ((Binary.Bplus (fprec t) (femax t) (fprec_gt_0 t) (fprec_lt_femax t)
             (plus_nan t) BinarySingleNaN.mode_NE x y));
simpl; try discriminate.
Qed.

Lemma BPLUS_accurate' {NAN: Nans} :
  forall x y
  (FIN: Binary.is_finite _ _ (BPLUS x y) = true),
  exists delta,
   Rabs delta <= D /\
   (@FT2R t (BPLUS x y ) = (FT2R x + FT2R y) * (1+delta))%R.
Proof.
intros.
assert (A: Binary.is_finite (fprec t) (femax t) x = true /\
  Binary.is_finite (fprec t) (femax t) y = true).
{ destruct x; destruct y; simpl; try discriminate; auto;
  destruct s; destruct s0; simpl; try discriminate; auto. }
destruct A as (A & B).
pose proof BPLUS_accurate x A y B (is_finite_sum_no_overflow x y FIN);
  auto.
Qed.

End GenFloat.


text:
Require Import Relations.
Module Type DEC_ORDER.
  Parameter A : Type.
  Parameter le : A -> A -> Prop.
  Parameter lt : A -> A -> Prop.

  Axiom ordered : order A le.
  Axiom lt_le_weak : forall a b:A, lt a b ->  le a b.
  Axiom lt_diff : forall a b:A, lt a b -> a <> b.
  Axiom le_lt_or_eq : forall a b:A, le a b -> lt a b \/ a = b.
  Parameter lt_eq_lt_dec :
    forall a b:A, {lt a b}+{a = b}+{lt b a}.
End DEC_ORDER.

Print order.
(*
Record order (A : Type) (R : relation A) : Prop := Build_order
  { ord_refl : reflexive A R;
    ord_trans : transitive A R;
    ord_antisym : antisymmetric A R }
*)

Check Build_order.
(*
Build_order
     : forall (A : Type) (R : relation A),
       reflexive A R -> transitive A R -> antisymmetric A R -> order A R
*)

Module Type MORE_DEC_ORDERS.
  Parameter A : Type.
  Parameter le: A -> A -> Prop.
  Parameter lt: A -> A -> Prop.

  Axiom le_trans: transitive A le.
  Axiom le_refl: reflexive A le.
  Axiom le_antisym: antisymmetric A le.
  Axiom lt_irreflexive: forall a:A, ~lt a a.
  Axiom lt_trans: transitive A lt.
  Axiom lt_not_le: forall a b:A, lt a b -> ~le b a.
  Axiom le_not_lt: forall a b:A, le a b -> ~lt b a.
  Axiom lt_intro: forall a b:A, le a b -> a <> b -> lt a b.

  Parameter le_lt_dec: forall a b:A, {le a b}+{lt b a}.
  Parameter le_lt_eq_dec: forall a b:A, le a b -> {lt a b}+{a = b}.
End MORE_DEC_ORDERS.

(* Writing a functor between DEC_ORDER and MORE_DEC_ORDERS *)
Module More_Dec_Orders (P:DEC_ORDER) :
                        MORE_DEC_ORDERS
                        with Definition A := P.A
                        with Definition le := P.le
                        with Definition lt := P.lt.

  Definition A := P.A.
  Definition le := P.le.
  Definition lt := P.lt.

  (* low level proof *)
  Theorem le_trans : transitive A le.
  Proof.
    generalize P.ordered. intro H. elim H.
      clear H. intros. simpl. unfold A, le. assumption.
  Qed.

  (* high level proof *)
  Theorem le_refl: reflexive A le.
  Proof.
    case P.ordered. intros. auto.
  Qed.

  Theorem le_antisym: antisymmetric A le.
  Proof.
    case P.ordered. intros. auto.
  Qed.

  Theorem lt_intro: forall a b:A, le a b -> a <> b -> lt a b.
  Proof.
    intros a b H diff. generalize (P.le_lt_or_eq a b H). intro H0. elim H0.
      clear H0. intro H0. unfold lt. exact H0.
      clear H0. intro H0. apply False_ind, diff. exact H0.
  Qed.

  Theorem lt_irreflexive: forall a:A, ~lt a a.
  Proof.
    intros a H. generalize (P.lt_diff a a H). intro H0. apply H0. reflexivity.
  Qed.

  Theorem lt_not_le: forall a b:A, lt a b -> ~le b a.
  Proof.
    intros a b H0 H1. cut (a = b). intro Hab. rewrite Hab in H0.
    apply (lt_irreflexive b). exact H0.
    apply P.lt_le_weak in H0. apply le_antisym. exact H0. exact H1.
  Qed.

  Theorem le_not_lt: forall a b:A, le a b -> ~lt b a.
  Proof.
    intros a b H0 H1. cut (a = b). intro Hab. rewrite Hab in H1.
    apply (lt_irreflexive b). exact H1.
    apply P.lt_le_weak in H1. apply le_antisym.  exact H0. exact H1.
  Qed.

  Theorem lt_trans: transitive A lt.
  Proof.
    unfold transitive. intros a b c Hab Hbc. generalize (P.lt_eq_lt_dec a c).
    intro H. elim H. clear H. intro H. elim H.
      clear H. intro H. exact H.
      clear H. intro H. rewrite <- H in Hbc. apply False_ind.
        cut (a=b). intro Eq. rewrite Eq in Hab. apply
        (lt_irreflexive b). exact Hab. apply le_antisym.
        apply P.lt_le_weak in Hab. exact Hab.
        apply P.lt_le_weak in Hbc. exact Hbc.
      clear H. intro H. apply False_ind. apply (lt_irreflexive c).
      cut (a=c). intro Hac. rewrite Hac in H. exact H.
      apply le_antisym. apply (le_trans a b c).
      apply P.lt_le_weak. exact Hab.
      apply P.lt_le_weak. exact Hbc.
      apply P.lt_le_weak. exact H.
  Qed.

  Definition le_lt_dec: forall a b:A, {le a b}+{lt b a}.
    intros a b. generalize (P.lt_eq_lt_dec a b). intro H.
    elim H. clear H. intro H. elim H.
      clear H. intro H. left. apply P.lt_le_weak. exact H.
      clear H. intro H. left. rewrite H. apply le_refl.
      clear H. intro H. right. exact H.
  Defined.

  Definition le_lt_eq_dec: forall a b:A, le a b -> {lt a b}+{a = b}.
    intros a b H. generalize (P.lt_eq_lt_dec a b).
    intro H0. elim H0. clear H0. intro H0. elim H0.
      clear H0. intro H0. left. exact H0.
      clear H0. intro H0. right. exact H0.
      clear H0. intro H0. right. apply le_antisym. exact H.
        apply P.lt_le_weak. exact H0.
  Defined.

End More_Dec_Orders.

Module Lexico (D1:DEC_ORDER)(D2:DEC_ORDER) <:
              DEC_ORDER with Definition A := (D1.A*D2.A)%type.

  Open Scope type_scope.

  Module M1:= More_Dec_Orders D1. (* calling previously defined functor *)
  Module M2:= More_Dec_Orders D2.

  Definition A:= D1.A*D2.A.
  Definition le (a b:A): Prop :=  (* lexicographic order *)
    let (a1, a2) := a in
    let (b1, b2) := b in D1.lt a1 b1 \/ a1 = b1 /\ D2.le a2 b2.
  Definition lt (a b:A): Prop :=
    let (a1, a2) := a in
    let (b1, b2) := b in D1.lt a1 b1 \/ a1 = b1 /\ D2.lt a2 b2.
  Theorem ordered: order A le.
  Proof.

author: possientis

repo: Prog

save_path: github-repos/coq/possientis-Prog


text:
(** This file is part of CoqEAL, the Coq Effective Algebra Library.
(c) Copyright INRIA and University of Gothenburg, see LICENSE *)
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq path.
From mathcomp Require Import ssralg fintype perm choice matrix bigop zmodp mxalgebra poly.

Require Import ssrcomplements dvdring stronglydiscrete.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import GRing.Theory.

Local Open Scope ring_scope.

Declare Scope mxpresentation_scope.
Delimit Scope mxpresentation_scope with MP.
Local Open Scope mxpresentation_scope.

(** Coherent rings *)
Module CoherentRing.

Record mixin_of (R : ringType) : Type := Mixin {
  dim_ker : forall m n, 'M[R]_(m,n) -> nat;
  ker : forall m n (M : 'M_(m,n)), 'M_(dim_ker M,m);
  _ : forall m n (M : 'M_(m,n)) (X : 'rV_m),
      reflect (exists Y, X = Y *m ker M) (X *m M == 0)
}.

Section ClassDef.

(** Coherent rings are based on strongly discrete rings *)
Record class_of (R : Type) : Type := Class {
  base  : StronglyDiscrete.class_of R;
  mixin : mixin_of (StronglyDiscrete.Pack base)
}.
Local Coercion base : class_of >-> StronglyDiscrete.class_of.

Structure type : Type := Pack {sort : Type; _ : class_of sort}.
Local Coercion sort : type >-> Sortclass.

Variable (T : Type) (cT : type).
Definition class := let: Pack _ c := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c.

Definition pack b0 (m0 : mixin_of (@StronglyDiscrete.Pack T b0)) :=
  fun bT b & phant_id (StronglyDiscrete.class bT) b =>
  fun    m & phant_id m m0 => Pack (@Class T b m).

Definition eqType := Equality.Pack class.
Definition choiceType := Choice.Pack class.
Definition zmodType := GRing.Zmodule.Pack class.
Definition ringType := GRing.Ring.Pack class.
Definition comRingType := GRing.ComRing.Pack class.
Definition unitRingType := GRing.UnitRing.Pack class.
Definition comUnitRingType := GRing.ComUnitRing.Pack class.
Definition idomainType := GRing.IntegralDomain.Pack class.
Definition stronglyDiscreteType := StronglyDiscrete.Pack class.

End ClassDef.

Module Exports.
Coercion base : class_of >-> StronglyDiscrete.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Bind Scope ring_scope with sort.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Coercion stronglyDiscreteType : type >-> StronglyDiscrete.type.
Canonical Structure stronglyDiscreteType.

Notation coherentRingType := type.
Notation CoherentRingType T m := (@pack T _ m _ _ id _ id).
Notation CoherentRingMixin := Mixin.
Notation "[ 'coherentRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
  (at level 0, format "[ 'coherentRingType'  'of'  T  'for'  cT ]") : form_scope.
Notation "[ 'coherentRingType' 'of' T ]" := (@clone T _ _ id)
  (at level 0, format "[ 'coherentRingType'  'of'  T ]") : form_scope.
End Exports.

End CoherentRing.
Export CoherentRing.Exports.

Definition dim_ker R := CoherentRing.dim_ker (CoherentRing.class R).
Definition ker R (m n : nat) (M : 'M_(m, n)) :'M_(dim_ker M, m) :=
  @CoherentRing.ker _ (CoherentRing.class R) m n M.

Section CoherentRingTheory.

Variable R : coherentRingType.

Lemma kerP_subproof : forall m n (M : 'M[R]_(m,n)) (X : 'rV_m),
  reflect (exists Y : 'rV_(dim_ker M), X = Y *m ker M) (X *m M == 0).
Proof. by case: R => [? [? []]]. Qed.

Lemma kerK m n (M : 'M[R]_(m,n)) : ker M *m M = 0.
Proof.
rewrite -row_matrixP => i; rewrite row_mul row0.
by apply/eqP/kerP_subproof; exists (delta_mx 0 i); rewrite rowE.
Qed.

Lemma kerAK p m n (M : 'M_(m,n)) (N : 'M[R]_(p, _)) : N *m ker M *m M = 0.
Proof. by rewrite -mulmxA kerK mulmx0. Qed.

Lemma ker1 m : ker (1%:M : 'M[R]_m) = 0.
Proof. by rewrite -kerK mulmx1. Qed.

Lemma kerP m n k (M : 'M[R]_(m,n)) (X : 'M_(k, m)) :
  reflect (exists Y : 'M_(k, dim_ker M), X = Y *m ker M) (X *m M == 0).
Proof.
apply: (iffP eqP); last first.
  case=> [Y ->]; apply/row_matrixP => i.
  by rewrite !row_mul row0 kerAK.
move=> XM0; have XM0_ i : row i X *m M == 0 by rewrite -row_mul XM0 row0.
exists (\matrix_(i, j) (projT1 (sig_eqW (kerP_subproof _ _ (XM0_ i)))) 0 j).
by apply/row_matrixP => i; rewrite row_mul rowK; case: sig_eqW.
Qed.

(** As everything is based on strongly discrete rings we can solve q systems
    of the kind XM = B *)
Fixpoint divmx m n l : 'M_(l, n) -> 'M[R]_(m, n) -> 'M_(l, m) :=
  if n is p.+1 return 'M_(l, n) -> 'M_(m, n) -> 'M_(l, m) then
    fun (B: 'M_(_, 1 + _)) (M : 'M_(_, 1 + _)) =>
      let K := ker (lsubmx M) in let W := divid (lsubmx B) (lsubmx M) in
      divmx (rsubmx B - W *m rsubmx M) (K *m rsubmx M) *m K + W
  else fun _ _ => 0.

Definition dvdmx m n k (M : 'M[R]_(m,n)) (N : 'M_(k, n)) :=
  divmx N M *m M == N.

Local Notation "M %| B" := (dvdmx M B) : mxpresentation_scope.

Lemma dvdmxP m n l (M : 'M[R]_(m, n)) (B : 'M_(l, n)) :
  reflect (exists X, B = X *m M) (M %| B).
Proof.
apply: (iffP eqP)=> [<-|[X -> {B}]]; first by eexists.
elim: n => //= [|n ihn] in m l M X *; first by apply/matrixP => i [].
rewrite -[n.+1]/(1 + n)%N in M X *.
set Ml := lsubmx M; set K := ker _; set W := divid _ _; set k := dim_ker _.
rewrite mulmxDl -mulmxA -!mulmx_rsub -!mulmxBl; apply: canLR (@addrNK _ _) _.
set Mr := rsubmx M; rewrite -mulmxBl -[M]hsubmxK -/Mr -/Ml !mul_mx_row.
have /kerP [Y ->] : (X - W) *m Ml == 0.
  by rewrite mulmxBl dividK -mulmx_lsub ?subrr ?subidMl.
by rewrite -!mulmxA !kerK !mulmx0 ihn.
Qed.

Lemma divmxK m n l (M : 'M[R]_(m, n)) (B : 'M_(l, n)) :
  M %| B -> divmx B M *m M = B.
Proof. by move/eqP. Qed.

Lemma sub_kermxP p m n (A : 'M_(m, n)) (B : 'M_(p, m)) :
  reflect (B *m A = 0) (ker A %| B).
Proof.
apply: (iffP (dvdmxP _ _)); last by move=> /eqP /kerP [X ->]; eexists.
by case=> D ->; rewrite -mulmxA kerK mulmx0.
Qed.

Lemma dvdmx_refl m n (M : 'M[R]_(m,n)) : M %| M .
Proof. by apply/dvdmxP; exists 1%:M; rewrite mul1mx. Qed.
Hint Resolve dvdmx_refl : core.

Lemma dvdmxMl m0 m1 m2 m3 (M : 'M[R]_(m1,m2)) (N : 'M[R]_(m3,m2))
  (K : 'M[R]_(m0,m3)) : M %| N -> M %| K *m N.
Proof.
by case/dvdmxP=> X hX; apply/dvdmxP; exists (K *m X); rewrite -mulmxA hX.
Qed.

Lemma dvdmx_trans m0 m1 m2 m3
  (M : 'M[R]_(m0,m1)) (N : 'M[R]_(m2,m1)) (K : 'M_(m3,m1)) :
  M %| N -> N %| K -> M %| K.
Proof. by move=> /dvdmxP [X ->] /dvdmxP [Y ->]; rewrite mulmxA dvdmxMl. Qed.

Lemma dvdmx0 k m n (M : 'M[R]_(m,n)) : M %| (0 : 'M[R]_(k,n)).
Proof. by apply/dvdmxP; exists 0; rewrite mul0mx. Qed.
Hint Resolve dvdmx0 : core.

Lemma dvd1mx m n (M : 'M[R]_(m,n)) : 1%:M %| M.
Proof. by apply/dvdmxP; exists M; rewrite mulmx1. Qed.
Hint Resolve dvd1mx : core.

Lemma dvd0mx k m n (M : 'M[R]_(m,n)) :
  ((0 : 'M[R]_(k,n)) %| M) = (M == 0).
Proof. by apply/idP/eqP => [/dvdmxP [X ->]|-> //]; rewrite mulmx0. Qed.

Lemma dvdmxMr (m0 m1 m2 m3 : nat) (K : 'M_(m2, m0))
     (M : 'M[R]_(m1, m2)) (N : 'M_(m3, m2)) :
   (M %| N) -> (M *m K %| N *m K).
Proof.
by case/dvdmxP=>X hX; apply/dvdmxP; exists X; rewrite mulmxA hX.
Qed.

Lemma dvdmxD m0 m1 m2 (M : 'M[R]_(m0,m1)) (N K : 'M[R]_(m2,m1)) :
  M %| N -> M %| K -> M %| N + K.
Proof. by move=> /dvdmxP [X ->] /dvdmxP [Y ->]; rewrite -mulmxDl dvdmxMl. Qed.

Lemma dvdmxN m0 m1 m2 (M : 'M[R]_(m0,m1)) (N : 'M[R]_(m2,m1)) :
  (M %| - N) = (M %| N).
Proof.
by apply/dvdmxP/dvdmxP=> [] [X hX]; exists (- X); rewrite mulNmx -hX ?opprK.
Qed.

Lemma dvdmxDr (m0 m1 m2 : nat)  (N K : 'M_(m2, m1)) (M : 'M[R]_(m0, m1)) :
  M %| N -> (M %| N + K) = (M %| K) :> bool.
Proof.
move=> dvdMN; apply/idP/idP; last exact: (dvdmxD dvdMN).
by rewrite -dvdmxN in dvdMN => /(dvdmxD dvdMN); rewrite addKr.
Qed.

Lemma dvdmxDl (m0 m1 m2 : nat) (N K : 'M_(m2, m1)) (M : 'M[R]_(m0, m1)) :
  M %| N -> (M %| K + N) = (M %| K) :> bool.
Proof. by rewrite addrC => /dvdmxDr ->. Qed.

Lemma dvdmxBr (m0 m1 m2 : nat)  (N K : 'M_(m2, m1)) (M : 'M[R]_(m0, m1)) :
  M %| N -> (M %| N - K) = (M %| K) :> bool.
Proof. by move=> dvdMN; rewrite dvdmxDr // dvdmxN. Qed.

Lemma dvdmxBl (m0 m1 m2 : nat) (N K : 'M_(m2, m1)) (M : 'M[R]_(m0, m1)) :
  M %| N -> (M %| K - N) = (M %| K) :> bool.
Proof. by move=> dvdMN; rewrite dvdmxDl // dvdmxN. Qed.

Lemma dvdmxB m0 m1 m2 (M : 'M[R]_(m0,m1)) (N K : 'M[R]_(m2,m1)) :
  M %| N -> M %| K -> M %| N - K.
Proof. by move=> /dvdmxBr ->. Qed.

Lemma dvdNmx m0 m1 m2 (M : 'M[R]_(m0,m1)) (N : 'M[R]_(m2,m1)) :
  (- M %| N) = (M %| N).
Proof.
by apply/dvdmxP/dvdmxP=> [] [X ->]; exists (- X); rewrite mulmxN mulNmx ?opprK.
Qed.

Definition ker_mod m0 m1 m2 (M : 'M[R]_(m0,m2)) (N : 'M[R]_(m1,m2)) :=
  rsubmx (ker (col_mx M N)).

Local Notation "M .-ker" := (ker_mod M)
  (at level 10, format "M .-ker") : mxpresentation_scope.

Lemma dvd_ker k m0 m1 m2
  (M : 'M[R]_(m0,m2)) (N : 'M[R]_(m1,m2)) (X : 'M_(k, m1)) :
   (M.-ker N %| X) = (M %| X *m N).
Proof.
apply/dvdmxP/dvdmxP.
  move=> [Y ->]; exists (- (Y *m lsubmx (ker (col_mx M N)))).
  apply/eqP; rewrite mulNmx -addr_eq0 addrC -!mulmxA -mulmxDr -mul_row_col.
  by rewrite hsubmxK kerK mulmx0.
case=> [Y /eqP]; rewrite eq_sym -subr_eq0 -mulNmx -mul_row_col.
move=> /kerP [Z /(congr1 rsubmx)]; rewrite row_mxKr -mulmx_rsub => HZ.
by exists (-Z); rewrite mulNmx -HZ opprK.
Qed.

Lemma dvd_ker_mod_ker m0 m1 m2 (M : 'M[R]_(m0,m2)) (N : 'M[R]_(m1,m2)) :
  (M.-ker N %| ker N).
Proof. by rewrite dvd_ker kerK dvdmx0. Qed.

Lemma dvd_ker_mod_1 m0 m1 m2 (M : 'M[R]_(m0,m2)) (N : 'M[R]_(m1,m2)) :
   (M.-ker N %| 1%:M) = (M %| N).
Proof. by rewrite dvd_ker mul1mx. Qed.

Lemma ker_modK m0 m1 m2 (M : 'M[R]_(m0,m2)) (N : 'M[R]_(m1,m2)) :
   (M %| M.-ker N *m N).
Proof. by rewrite -dvd_ker. Qed.

Lemma ker_mod1 m0 m1 (M : 'M[R]_(m0,m1)) : M %| M.-ker 1%:M.
Proof.
rewrite -dvdNmx; apply/dvdmxP; exists (lsubmx (ker (col_mx M 1%:M))).
apply/eqP; rewrite mulmxN -addr_eq0 addrC -[M.-ker _]mulmx1 -mul_row_col.
by rewrite hsubmxK kerK.
Qed.

Lemma dvd_mx_col k m0 m1 m2
  (M : 'M[R]_(m0,m2)) (N : 'M[R]_(m1,m2)) (X : 'M_(k, m2)) :
   (X %| col_mx M N) = (X %| M) && (X %| N).
Proof.
apply/dvdmxP/andP=> [[Y]|[/dvdmxP [M' ->] /dvdmxP [N' ->]]]; last first.
  by exists (col_mx M' N'); rewrite mul_col_mx.
rewrite -[Y]vsubmxK mul_col_mx => HY.
have := (congr1 usubmx HY, congr1 dsubmx HY).
by rewrite !col_mxKu !col_mxKd => [[-> ->]]; rewrite !dvdmxMl.
Qed.

Lemma dvd_col_mxP k m0 m1 m2
  (M : 'M[R]_(m0,m2)) (N : 'M[R]_(m1,m2)) (X : 'M_(k, m2)) :
   reflect (exists Y, M %| X - Y *m N) (col_mx M N %| X).
Proof.
apply: (iffP (dvdmxP _ _)) => [[Y ->]|[Y /dvdmxP [Z HZ]]]; last first.
  by exists (row_mx Z Y); rewrite mul_row_col -HZ addrNK.
exists (rsubmx Y).
by rewrite -[Y as Y' in Y' *m _]hsubmxK mul_row_col addrK dvdmxMl.
Qed.

Lemma dvd_col_mxl m0 m1 m2 (M : 'M[R]_(m0, m2)) (N : 'M_(m1, m2)) :
  col_mx M N %| N.
Proof. by apply/dvd_col_mxP; exists 1%:M; rewrite mul1mx subrr. Qed.

Lemma dvd_col_mxu m0 m1 m2 (M : 'M[R]_(m0, m2)) (N : 'M_(m1, m2)) :
  col_mx M N %| M.
Proof. by apply/dvd_col_mxP; exists 0; rewrite mul0mx subr0. Qed.

End CoherentRingTheory.

Notation "M .-ker" := (ker_mod M)
  (at level 10, format "M .-ker") : mxpresentation_scope.
Notation "M %| B" := (dvdmx M B) : mxpresentation_scope.

#[export] Hint Resolve dvdmx_refl dvdmx0 dvd1mx : core.

(* It suffices to show how to solve xM = 0 when M is a column for the ring to
   be coherent *)
Section ker_col.

Variable R : comRingType.

Variable dim_ker_col : forall m, 'cV[R]_m -> nat.
Variable ker_col : forall m (M : 'cV[R]_m), 'M[R]_(dim_ker_col M,m).
Hypothesis ker_colP : forall m (M : 'cV_m) (X : 'rV_m),
  reflect (exists Y , X = Y *m ker_col M) (X *m M == 0).

Fixpoint dim_ker_c m n : 'M[R]_(m,n) -> nat :=
  if n is p.+1 then
    fun (M: 'M[R]_(m,1 + _)) =>
      dim_ker_c (ker_col (lsubmx M) *m rsubmx M)
  else fun => m.

Fixpoint ker_c m n : forall (M : 'M_(m,n)), 'M_(dim_ker_c M,m) :=
  if n is p.+1 then
    fun (M : 'M_(m,1 + _)) =>
      let G1 := ker_col (lsubmx M) in
      ker_c (G1 *m rsubmx M) *m G1
  else fun => 1%:M.

Lemma ker_cP : forall m n (M : 'M[R]_(m,n)) (X : 'rV_m),
  reflect (exists Y, X = Y *m ker_c M) (X *m M == 0).
Proof.
move=> m n; elim: n m=> [n m X | n ih m].
  by rewrite ?thinmx0; apply: (iffP idP)=> //= _; exists X; rewrite mulmx1.
rewrite [n.+1]/(1 + n)%nat => M /=; set G1 := ker_col (lsubmx M).
move: (ih _ (G1 *m rsubmx M))=> {}ih X.
apply: (iffP eqP)=> [|[Y hY]];
  rewrite -{1}[M]hsubmxK (@mul_mx_row _ _ _ 1) -(@row_mx0 _ _ 1).
  case/(@eq_row_mx _ _ 1); case/eqP/ker_colP=> V ->; rewrite -mulmxA.
  by case/eqP/ih=> W ->; exists W; rewrite mulmxA.
f_equal; apply/eqP.
  by apply/ker_colP; exists (Y *m ker_c (G1 *m rsubmx M)); rewrite -mulmxA.
by rewrite hY mulmxA -[_ *m rsubmx M]mulmxA; apply/ih; exists Y.
Qed.

End ker_col.

Lemma kerE (R : coherentRingType) m n (M : 'M[R]_(m, n)) :
   ker M = castmx (congr1 _ (col_0mx _), erefl) (0.-ker M).
Proof.
rewrite /(0.-ker) -(esymK (col_0mx _)).
case: _ / (esym (col_0mx _)); rewrite castmx_id.
by apply/matrixP => i j; rewrite mxE /=; congr (ker M _ _); apply: val_inj.
Qed.

(** This section proves that a ring is coherent is the intersection of two *)
(*    finitely generated ideals is again finitely generated. It requires that *)
(*    the underlying ring (in this case a strongly discrete ring) is an *)
(*    integral domain *)
Section IntersectionCoherent.

Variable R : stronglyDiscreteType.

(** The size of the intersection - 1, this is done to ensure that *)
(*    the intersection is nonempty *)
Variable dim_cap : forall m n, 'cV[R]_m -> 'cV[R]_n -> nat.

(** Intersection of two ideals *)
Variable cap :
  forall n m (I : 'cV[R]_n) (J : 'cV[R]_m), 'cV[R]_(dim_cap I J).+1.

Hypothesis cap_spec : forall n m (I : 'cV[R]_n) (J : 'cV[R]_m),
  int_spec (cap I J).

Fixpoint dim_int n : 'cV[R]_n -> nat :=
  if n is p.+1 then
    fun (V : 'cV[R]_(1 + p)) =>
      let v  := usubmx V in
      let vs := dsubmx V : 'cV[R]_p in
      ((dim_cap v (-vs)).+1 + dim_int vs)%N
  else fun => 0%N.

Definition cap_wl n m (I : 'cV_n) (J : 'cV_m) := divid (cap I J) I.

Lemma wl n m (I : 'cV_n) (J : 'cV_m) : cap_wl I J *m I = cap I J.
Proof. by apply: dividK; case: cap_spec. Qed.

Definition cap_wr n m (I : 'cV_n) (J : 'cV_m) := divid (cap I J) J.

Lemma wr n m (I : 'cV_n) (J : 'cV_m) : cap_wr I J *m J = cap I J.
Proof. by apply: dividK; case: cap_spec. Qed.

Fixpoint ker_c_int m : forall (V : 'cV_m),'M_(dim_int V,m) :=
  if m is p.+1 return forall V : 'cV_m, 'M_(dim_int V,m) then
    fun (V' : 'cV_(1 + p)) =>
      let v   := usubmx V' in
      let vs  := dsubmx V' in
      let m0  := ker_c_int vs in
      let wv  := cap_wl v (-vs) in
      let wvs := cap_wr v (-vs) in
      block_mx (if v == 0 then delta_mx 0 0 else wv) (if v == 0 then 0 else wvs)
               0           m0
  else fun => 0.

(* TODO: Move to ssrcomplements *)
Lemma colE m n (i : 'I_n) (M : 'M[R]_(m, n)) :
  col i M = M *m delta_mx i 0.
Proof. by apply/trmx_inj; rewrite trmx_mul trmx_delta -rowE tr_col. Qed.

Lemma ker_c_intP : forall m (V : 'cV_m) (X : 'rV_m),
  reflect (exists Y, X = Y *m ker_c_int V) (X *m V == 0).
Proof.
elim => [V X | n IH] /=.
  rewrite thinmx0 flatmx0 /ker_c_int mulmx0 eqxx.
  by constructor; exists 0; rewrite mulmx0.
rewrite [n.+1]/(1 + n)%nat => V X.
set v  := usubmx V.
set vs := dsubmx V.
set x  := lsubmx X.
set xs := rsubmx X.
set m0 := ker_c_int vs.
set wv := cap_wl v (-vs).
set wvs := cap_wr v (-vs).
move: (wl v (-vs)); rewrite -/wv => Hwv.
move: (wr v (-vs)); rewrite -/wvs => Hwvs.
rewrite -[V]vsubmxK -[X]hsubmxK.
case: (eqVneq v 0) => v0.
  apply: (iffP idP) => /= [|[W ->]].
    rewrite (@mul_row_col _ _ 1) -/v v0 mulmx0 add0r => vs0.
    case: (IH vs xs) => [[A HA]|[]]; last by apply/IH.
    exists (row_mx (const_mx (x 0 0)) A).
    rewrite (@mul_row_block _ _ _ _ 1) -/xs !mulmx0 add0r addr0 -colE col_const HA.
    by f_equal; apply/rowP => i; rewrite !mxE /= !ord1.
  rewrite -mulmxA (@mul_block_col _ _ _ 1) -/v !mul0mx addr0 add0r.
  rewrite -[W]hsubmxK mul_row_col {6}v0 !mulmx0 add0r mulmxA.
  by apply/IH; exists (rsubmx W).
apply: (iffP idP) => /= [|[W ->]].
  rewrite (@mul_row_col _ _ 1) => hwx.
  have vx00 : ((x * v) 0 0)%:M = x * v.
    by apply/matrixP=> i j; rewrite !ord1 !mxE eqxx.
  have : member ((x * v) 0 0) (cap v (- vs)).
    case: cap_spec => c /= _ _ in_int.
    apply: in_int; first by apply/memberP; exists x; rewrite vx00.
    apply/memberP; exists xs; apply/eqP.
    move: hwx; rewrite -/v -/vs -/x -/xs mulmxN addr_eq0 => /eqP <-.
    by rewrite vx00.
  case/memberP=> W hW.
  case: (IH vs (xs - (W *m wvs))) => [[A HA]|[]].
    exists (row_mx W A).
    rewrite (@mul_row_block _ _ _ _ 1) mulmx0 addr0 -HA addrCA subrr addr0.
    f_equal; apply/(@scalemx_inj _ _ _ (v 0 0)).
    (* The proof breaks down here if strongly discrete rings are not idomains! *)
      apply: contra_neq v0 => v00.
      by apply/rowP => i; rewrite !ord1 /= v00 !mxE.
    by rewrite -!mul_mx_scalar -mx11_scalar -mulmxA Hwv -hW -/x vx00.
  by apply/IH; rewrite mulmxDl mulNmx addrC -mulmxN -mulmxA Hwvs -hW vx00.
rewrite -[W]hsubmxK (@mul_row_block _ _ _ _ 1) mulmx0 addr0 (@mul_row_col _ _ 1).
rewrite -!mulmxA Hwv addr_eq0 -mulmxN mulmxDl -!mulmxA Hwvs addrC -subr_eq.
rewrite addrN -/vs !mulmxN eq_sym oppr_eq0 mulmxA.
case: (IH vs _) => // [[]].
by exists (rsubmx W).
Qed.

Definition int_coherentMixin := CoherentRing.Mixin (ker_cP ker_c_intP).
Canonical Structure int_coherentType :=
  Eval hnf in CoherentRingType R int_coherentMixin.

End IntersectionCoherent.

(* Using the above result one can prove that Bezout rings are coherent, however
   this is not what we want as we want to prove that constructive PIDs are
   coherent using smith *)
Section BezoutCoherent.

Variable R : bezoutDomainType.

Definition bdim_cap m n (I : 'cV[R]_m) (J : 'cV[R]_n) := 0%N.

Definition bcap m n (I : 'cV_m) (J : 'cV_n) : 'cV[R]_1 :=
  (lcmr (principal_gen I) (principal_gen J))%:M.

Definition bcap_wl m n (I : 'cV_m) (J : 'cV_n) : 'rV[R]_m :=
  let a := principal_gen I in
  let b := principal_gen J in
  (odflt 0 (b %/? gcdr a b))%:M *m principal_w1 I.

Lemma bcap_wlP m n (I : 'cV_m) (J : 'cV_n) : bcap_wl I J *m I = bcap I J.
Proof.
rewrite /bcap_wl /bcap -mulmxA principal_w1_correct mul_scalar_mx.
apply/rowP => i; rewrite !mxE !ord1 {i} /= !mulr1n.
set a := principal_gen _; set b := principal_gen _.
have [-> | b0] := eqVneq b 0; first by rewrite lcm0r mulr0.
have [-> | a0] := eqVneq a 0.
  by rewrite lcmr0 odiv0r /= ?mul0r // gcdr_eq0 negb_and b0.
case: odivrP => /= => [x Hx | H].
  apply/(@mulIf _ (gcdr b a)); first by rewrite gcdr_eq0 negb_and b0.
  by rewrite mulr_lcm_gcd -mulrA mulrCA -Hx.
case/dvdrP: (dvdr_gcdr b a) => x /eqP Hx.
by move: (H x); rewrite Hx.
Qed.

Definition bcap_wr m n (I : 'cV_m) (J : 'cV_n) : 'rV[R]_n :=
  let a := principal_gen I in
  let b := principal_gen J in
  (odflt 0 (a %/? (gcdr a b)))%:M *m principal_w1 J.

Lemma bcap_wrP n m (I : 'cV_n) (J : 'cV_m) : bcap_wr I J *m J = bcap I J.
Proof.
rewrite /bcap_wl /bcap -mulmxA principal_w1_correct mul_scalar_mx.
apply/rowP => i; rewrite !mxE !ord1 {i} /= !mulr1n.
set b := principal_gen _; set a := principal_gen _.
have [-> | a0] := eqVneq a 0; first by rewrite lcmr0 mulr0.
have [-> | b0] := eqVneq b 0.
  by rewrite lcm0r odiv0r /= ?mul0r // gcdr_eq0 negb_and eqxx.
case: odivrP => /= => [x Hx | H].
  apply/(@mulIf _ (gcdr b a)); first by rewrite gcdr_eq0 negb_and b0.
  by rewrite -mulrA mulrCA -Hx mulr_lcm_gcd mulrC.
case/dvdrP: (dvdr_gcdl b a) => x /eqP Hx.
by move: (H x); rewrite Hx.
Qed.

Lemma bcap_int (x : 'M_1) (m n : nat) (I : 'cV_m) (J : 'cV_n) :
  (exists I' : 'rV_m, I' *m I = x) ->
  (exists J' : 'rV_n, J' *m J = x) ->
   exists W : 'M_1, W *m bcap I J = x.
Proof.
case => I' HI' [J' HJ'].
move: (principal_w2_correct I).
move: (principal_w2_correct J).
rewrite /bcap /principal.
set a := principal_gen I; set b := principal_gen J => Hb Ha.
have div1 : (a %| x 0 0)%R.
  apply/dvdrP.
  exists ((I' *m principal_w2 I) 0 0).
  move: HI'.
  rewrite -{1}Ha => <-.
  by rewrite mulrC mul_mx_scalar -scalemxAr !mxE.
have div2 : (b %| x 0 0)%R.
  apply/dvdrP.
  exists ((J' *m principal_w2 J) 0 0).
  move: HJ'.
  rewrite -{1}Hb => <-.
  by rewrite mulrC mul_mx_scalar -scalemxAr !mxE.
move/dvdrP: (dvdr_lcm a b (x 0 0)).
rewrite div1 div2 /= => [[y Hy]].
exists y%:M.
by rewrite -scalar_mxM -Hy -mx11_scalar.
Qed.

(* This is a bit ugly... *)
Lemma bcap_spec m n (I : 'cV[R]_m) (J : 'cV[R]_n) :
  @int_spec _ _ m n I J (bcap I J).
Proof.
split.
- by apply/subidP; exists (bcap_wl I J); rewrite bcap_wlP.
- by apply/subidP; exists (bcap_wr I J); rewrite bcap_wrP.
move=> /= x.
case/memberP => I' hI'.
case/memberP => J' hJ'.
apply/memberP.
have h1 : exists I'0 : 'rV_m, I'0 *m I = x%:M by exists I'.
have h2 : exists J'0 : 'rV_n, J'0 *m J = x%:M by exists J'.
case: (bcap_int h1 h2) => D hD.
by exists D.
Qed.

Definition bezout_coherentMixin := int_coherentMixin bcap_spec.
Canonical Structure bezout_coherentType :=
  Eval hnf in CoherentRingType R bezout_coherentMixin.

End BezoutCoherent.

author: coq-community

repo: coqeal

save_path: github-repos/coq/coq-community-coqeal


text:
From Coq Require Import Classical ClassicalEpsilon.
From CasperCBC Require Import Lib.SsrExport Lib.Traces Lib.TraceProperties.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

(** * Properties of possibly-infinite traces requiring classical logic *)

Section TraceClassicalProperties.

Context {A B : Type}.

Local Notation trace := (@trace A B).
Local Notation propT := (@propT A B).

(** ** Relating finiteness and infiniteness *)

Lemma not_infiniteT_finiteT : forall tr : trace,
 ~ infiniteT tr -> finiteT tr.
Proof.
move => tr Hnot.
case (classic (finiteT tr)) => Hinf //.
case: Hnot.
exact: not_finiteT_infiniteT.
Qed.

Lemma finiteT_infiniteT : forall tr : trace,
 finiteT tr \/ infiniteT tr.
Proof.
move => tr.
case (classic (finiteT tr)) => Hinf; first by left.
right.
exact: not_finiteT_infiniteT.
Qed.

Definition finiteT_infiniteT_dec (tr : trace) : { finiteT tr }+{ infiniteT tr } :=
match excluded_middle_informative (finiteT tr) with
| left Hfin => left Hfin
| right Hfin => right (not_finiteT_infiniteT Hfin)
end.

(** ** Using midpoints to show the right associativity of the append property *)

CoFixpoint midp (p0 p1: trace -> Prop) tr0 tr1 (h: followsT (appendT p0 p1) tr0 tr1) : trace :=
match followsT_dec h with
| inl (existT tr (exist a (conj _ (conj _ H)))) =>
  let: exist x _ := constructive_indefinite_description _ H in x
| inr (existT tr (existT tr' (existT a (exist b (conj _ (conj _ H)))))) =>
  Tcons a b (@midp _ _ _ _ H)
end.

Lemma midpointT_midp : forall (p0 p1: trace -> Prop) tr0 tr1 (h : followsT (appendT p0 p1) tr0 tr1),
 midpointT h (midp h).
Proof.
cofix CIH.
dependent inversion h; subst.
- rewrite [midp _]trace_destr /=.
  case (constructive_indefinite_description _ _) => /=.
  move => x [a1 hm].
  by apply midpointT_nil => //; destruct x.
- rewrite [midp _]trace_destr /=.
  exact: (@midpointT_delay _ _ p0 p1 (Tcons a b tr) (Tcons a b tr') (followsT_delay a b f) tr tr' f a b (midp f)).
Qed.

Lemma appendT_assoc_R: forall p1 p2 p3,
 forall tr : trace, (appendT p1 (appendT p2 p3)) tr -> (appendT (appendT p1 p2)  p3) tr.
Proof.
move => p1 p2 p3 tr0 h1.  move: h1 => [tr1 [h1 h2]].
exists (midp h2). split.
- exists tr1; split => //.
  exact: (midpointT_before (midpointT_midp h2)).
- exact: (midpointT_after (midpointT_midp h2)).
Qed.

Lemma AppendT_assoc_R: forall (p1 p2 p3 : propT), (p1 *** p2 *** p3) =>> (p1 *** p2) *** p3.
Proof.
move => p1 p2 p3 tr0 h1. destruct p1 as [f1 hf1]. destruct p2 as [f2 hf2].
destruct p3 as [f3 hf3]. simpl. simpl in h1. apply appendT_assoc_R. by apply h1.
Qed.

End TraceClassicalProperties.

author: zunction

repo: casper-cbc-proofs


text:
Load LFindLoad.
From lfind Require Import LFind.
Unset Printing Notations.
Set Printing Implicit.

From QuickChick Require Import QuickChick.
Inductive natural : Type := Succ : natural -> natural |  Zero : natural.
Derive Show for natural. Derive Arbitrary for natural.  Instance Dec_Eq_natural : Dec_Eq natural. Proof. dec_eq. Qed.
Inductive lst : Type := Cons : natural -> lst -> lst |  Nil : lst.

Inductive tree : Type := Node : natural -> tree -> tree -> tree |  Leaf : tree.

Inductive Pair : Type := mkpair : natural -> natural -> Pair
with Zlst : Type := zcons : Pair -> Zlst -> Zlst |  znil : Zlst.

Fixpoint even (even_arg0 : natural) : bool
           := match even_arg0 with
              | Zero => true
              | Succ n => negb (even n)
              end.

Fixpoint append (append_arg0 : lst) (append_arg1 : lst) : lst
           := match append_arg0, append_arg1 with
              | Nil, x => x
              | Cons x y, z => Cons x (append y z)
              end.

Fixpoint len (len_arg0 : lst) : natural
           := match len_arg0 with
              | Nil => Zero
              | Cons x y => Succ (len y)
              end.

Lemma lem: forall l1 l2 n, negb (even (len (append l1 l2))) = even (len (append l1 (Cons n l2))).
Proof.
induction l1.
  - intros. simpl. rewrite (IHl1 l2 n0). reflexivity.
  - intros. simpl. reflexivity.
Qed.

Lemma lem3: forall l, append l Nil = l.
Proof.
induction l.
  - simpl. rewrite IHl. reflexivity.
  - reflexivity.
Qed.

Theorem theorem0 : forall (x : lst) (y : lst), eq (even (len (append x y))) (even (len (append y x))).
Proof.
induction x.
  - intros. simpl. rewrite <- lem. f_equal. rewrite IHx. reflexivity.
  - intros.  simpl. lfind.  reflexivity.
Admitted.

author: yalhessi

repo: lemmaranker

save_path: github-repos/coq/yalhessi-lemmaranker


text:
Require Import
  MathClasses.interfaces.abstract_algebra Coq.Logic.ChoiceFacts MathClasses.interfaces.functors
  MathClasses.theory.categories MathClasses.categories.categories.

(* Axiom dependent_functional_choice: DependentFunctionalChoice. *)

Section object.
  Context {I: Type} (O: I → Type)
    `{∀ i, Arrows (O i)}
    `{∀ i (x y: O i), Equiv (x ⟶ y)}
    `{∀ i, CatId (O i)} `{∀ i, CatComp (O i)}
    `{∀ i, Category (O i)}.

  Definition Object := ∀ i, O i.
  Global Instance pa: Arrows Object := λ x y, ∀ i, x i ⟶ y i. (* todo: make nameless *)
  Global Instance: CatId Object := λ _ _, cat_id.
  Global Instance: CatComp Object := λ _ _ _ d e i, d i ◎ e i.
  Definition e (x y: Object): Equiv (x ⟶ y) := λ f g, ∀ i, f i = g i.
End object.

(* Avoid Coq trying to apply e to find arbitrary Equiv instances *)
#[global]
Hint Extern 0 (Equiv (_ ⟶ _)) => eapply @e : typeclass_instances.

Section contents.
  Context {I: Type} (O: I → Type)
    `{∀ i, Arrows (O i)}
    `{∀ i (x y: O i), Equiv (x ⟶ y)}
    `{∀ i, CatId (O i)} `{∀ i, CatComp (O i)}
    `{∀ i, Category (O i)}.

  Global Instance: ∀ x y: Object O, Setoid (x ⟶ y) := _.

  Global Instance: Category (Object O).
  Proof with try reflexivity.
   constructor. apply _.
      intros ? ? ? x y E x' y' F i.
      change (x i ◎ x' i = y i ◎ y' i).
      rewrite (E i), (F i)...
     repeat intro. apply comp_assoc.
    repeat intro. apply id_l. (* todo: Use left_identity *)
   repeat intro. apply id_r.
  Qed.

  Let product_object := categories.object (Object O).

  Notation ith_obj i := (categories.object (O i)).

  Program Definition project i: categories.object (Object O) ⟶ ith_obj i :=
    @categories.arrow _ _ (λ d, d i) (λ _ _ a, a i) _.
  Next Obligation. Proof. (* functorial *)
   constructor; intros; try reflexivity; try apply _.
   constructor; try apply _.
   intros ? ? E. apply E.
  Qed.

  Section factors.

    Variables (C: categories.Object) (X: ∀ i, C ⟶ ith_obj i).

    Let ith_functor i := categories.Functor_inst _ _ (X i).
      (* todo: really necessary? *)

    Program Definition factor: C ⟶ product_object
      := @categories.arrow _ _ (λ (c: C) i, X i c) (λ (x y: C) (c: x ⟶ y) i, fmap (X i) c) _.
    Next Obligation. Proof with try reflexivity; intuition. (* functorial *)
     constructor; intros; try apply _.
       constructor; try apply _.
       intros ? ? E ?.
       change (fmap (X i) x = fmap (X i) y).
       rewrite E...
      intro. unfold fmap at 1. rewrite preserves_id... destruct X...
     intro. unfold fmap at 1. rewrite preserves_comp... destruct X...
    Qed. (* todo: those [destruct X]'s shouldn't be necessary *)
(*
    Lemma s: is_sole (λ h', ∀ i, X i = project i ◎ h') factor.
    Proof with try reflexivity; intuition.
     split.
      intro.
      exists (λ v, refl_arrows (X i v)).
      simpl. unfold compose. intros ? ? ?.
      rewrite right_identity, left_identity...
     intros alt alt_factors.
     generalize (dependent_functional_choice I _ _ alt_factors). clear alt_factors.
     unfold isoT in *.
     simpl.
     intros [x H4].
     unfold equiv.
     unfold categories.e.
     unfold compose in H4.
     set (P := λ v, prod (alt v ⟶ (λ i, (X i) v)) ((λ i, (X i) v) ⟶ alt v)).
     set (d := λ v, (λ i, snd (` (x i v)), λ i, fst (` (x i v))): P v).
     assert (∀ v, uncurry iso_arrows (d v)) as Q.
      split; simpl; intro.
       change (snd (` (x i v)) ◎ fst (` (x i v)) = cat_id).
       destruct (x i v) as [? []]...
      change (fst (` (x i v)) ◎ snd (` (x i v)) = cat_id).
      destruct (x i v) as [? []]...
     exists (λ v, exist (uncurry iso_arrows) _ (Q v)).
     intros p q r i.
     simpl.
     unfold comp.
     unfold CatComp_instance_0. (* todo: no! *)
     pose proof (H4 i p q r). clear H4.
     destruct (x i p) as [aa0 i0].
     destruct (x i q) as [a1a2 i1].
     simpl in *.
     unfold uncurry in *.
     unfold iso_arrows in *.
     destruct (categories.Functor_inst _ _ alt).
     unfold compose in x, aa0, a1a2.
     simpl in *.
     unfold fmap.
     match goal with
       |- appcontext [ categories.Fmap_inst _ ?cat ?alt ] => set (f:=categories.Fmap_inst _ cat alt) in |- *
     end.
     setoid_rewrite <- (left_identity (f p q r i ◎ fst aa0)).
     transitivity ((fst a1a2 ◎ snd a1a2) ◎ (f p q r i ◎ fst aa0)).
      apply comp_proper...
     apply transitivity with ((fst a1a2) ◎ (((snd a1a2) ◎ (categories.Fmap_inst _ _ alt p q r i)) ◎ (fst aa0))).
      repeat rewrite associativity...
     simpl.
     rewrite <- H5.
     repeat rewrite <- (associativity _ _).
     rewrite (proj2 i0), right_identity...
    Qed. (* WARNING: Uses DependentFunctionalChoice. (Todo: reflect.) *)
      (* todo: awful proof. clean up! *)
*)
  End factors.

  (* At the time of this writing (Coq trunk 12801), attempting to state the above in terms
  of the nice product-relates interfaces from theory/categories results in universe
  inconsistency errors that I have isolated and reported as Coq bug #2252. *)

  Global Instance mono (X Y: Object O): ∀ (a: X ⟶ Y), (∀ i, @Mono _ _ (H0 _) (H2 i) _ _ (a i)) → Mono a.
  Proof. firstorder. Qed. (* todo: why so ugly all of a sudden? *)

End contents.

repo: math-classes