FinMatrix.Matrix.ElementType

Require Export Hierarchy.

ElementType

A type with decidable equality and zero element

Module Type ElementType.
  Parameter A : Type.
  Parameter Azero : A.
  Notation "0" := Azero : A_scope.

  Axiom AeqDec : Dec (@eq A).
  #[export] Existing Instance AeqDec.
End ElementType.

Instances

Module ElementTypeFun (I O : ElementType) <: ElementType.
  Definition A : Type := I.A -> O.A.
  Definition Azero : A := fun _ => O.Azero.
  Hint Unfold A Azero : A.

  Lemma AeqDec : Dec (@eq A).
  Proof. constructor. intros a b. unfold A in *.
  Admitted.
End ElementTypeFun.

OrderedElementType

An extended `ElementType` equipped with order relation

Module Type OrderedElementType <: ElementType.
  Include ElementType.

  Parameter Alt Ale : A -> A -> Prop.

  Infix "<" := Alt : A_scope.
  Infix "<=" := Ale : A_scope.

  Axiom Order : Order Alt Ale.
End OrderedElementType.

Element with abelian-monoid structure

Type of Element with abelian-monoid structure

Module Type MonoidElementType <: ElementType.
  Include ElementType.
  Open Scope A_scope.

  Parameter Aadd : A -> A -> A.
  Infix "+" := Aadd : A_scope.

  Axiom Aadd_AMonoid : AMonoid Aadd Azero.
  #[export] Existing Instance Aadd_AMonoid.
End MonoidElementType.

Instances

Module MonoidElementTypeFun (I O : MonoidElementType) <: MonoidElementType.

  Include (ElementTypeFun I O).
  Open Scope A_scope.

  Definition Aadd (f g : A) : A := fun x : I.A => O.Aadd (f x) (g x).
  Hint Unfold Aadd : A.

  Infix "+" := Aadd : A_scope.

  Lemma Aadd_Associative : Associative Aadd.
  Proof.
    intros. constructor; intros; autounfold with A.
    extensionality x. apply O.Aadd_AMonoid.
  Qed.

  Lemma Aadd_Commutative : Commutative Aadd.
  Proof.
    intros. constructor; intros; autounfold with A.
    extensionality x. apply O.Aadd_AMonoid.
  Qed.

  Lemma Aadd_IdentityLeft : IdentityLeft Aadd Azero.
  Proof.
    intros. constructor; intros; autounfold with A.
    extensionality x. apply O.Aadd_AMonoid.
  Qed.

  Lemma Aadd_IdentityRight : IdentityRight Aadd Azero.
  Proof.
    intros. constructor; intros; autounfold with A.
    extensionality x. apply O.Aadd_AMonoid.
  Qed.

  #[export] Instance Aadd_AMonoid : AMonoid Aadd Azero.
  Proof.
    intros. constructor; intros; autounfold with A.
    intros. constructor; intros; autounfold with A.
    constructor. apply Aadd_Associative.
    apply Aadd_IdentityLeft. apply Aadd_IdentityRight.
    constructor. apply Aadd_Associative.
    apply Aadd_Commutative.
    constructor. constructor. apply Aadd_Associative.
    apply Aadd_Commutative.
  Qed.
End MonoidElementTypeFun.

Element with abelian-ring structure

Type of Element with abelian-ring structure

Module Type RingElementType <: MonoidElementType.
  Include MonoidElementType.
  Open Scope A_scope.

  Parameter Aone : A.
  Parameter Amul : A -> A -> A.
  Parameter Aopp : A -> A.

  Notation Asub := (fun x y => Aadd x (Aopp y)).
  Infix "*" := Amul : A_scope.
  Notation "1" := Aone : A_scope.
  Notation "a ²" := (a * a) : A_scope.
  Notation "- a" := (Aopp a) : A_scope.
  Infix "-" := Asub : A_scope.

A Ring structure can be derived from the context

Axiom ARing : ARing Aadd 0 Aopp Amul 1.

#[export] Existing Instance ARing.

End RingElementType.

Instances

Module RingElementTypeFun (I O : RingElementType) <: RingElementType.
  Add Ring Ring_thy_inst_o : (make_ring_theory O.ARing).

  Include (MonoidElementTypeFun I O).

  Definition Aone : A := fun _ => O.Aone.
  Definition Aopp (f : A) : A := fun x : I.A => O.Aopp (f x).
  Definition Amul (f g : A) : A := fun x : I.A => O.Amul (f x) (g x).
  Notation Asub := (fun x y => Aadd x (Aopp y)).

  #[export] Instance ARing : ARing Aadd Azero Aopp Amul Aone.
  Proof.
    repeat constructor; autounfold with A; intros;
      apply functional_extensionality; intros; cbv; ring.
  Qed.

  Add Ring Ring_inst : (make_ring_theory ARing).
End RingElementTypeFun.

Element with abelian-ring structure and ordered relation

Type of Element with ordered abelian-ring structure

Module Type OrderedRingElementType <: RingElementType <: OrderedElementType.
  Include RingElementType.

  Parameter Alt Ale : A -> A -> Prop.

  Infix "<" := Alt : A_scope.
  Infix "<=" := Ale : A_scope.

  Axiom Order : Order Alt Ale.
  Axiom OrderedARing : OrderedARing Aadd Azero Aopp Amul Aone Alt Ale.
  #[export] Existing Instance OrderedARing.

  Notation "| a |" := (Aabs a) : A_scope.

End OrderedRingElementType.

Instances

Element with field structure

Type of Element with field structure

Module Type FieldElementType <: RingElementType.
  Include RingElementType.
  Open Scope A_scope.

  Parameter Ainv : A -> A.

  Notation Adiv := (fun x y => Amul x (Ainv y)).
  Notation "/ a" := (Ainv a) : A_scope.
  Infix "/" := Adiv : A_scope.

1 <> 0.

  Axiom Aone_neq_Azero : Aone <> Azero.

  Axiom Field : Field Aadd Azero Aopp Amul Aone Ainv.

  #[export] Existing Instance Field.
End FieldElementType.

Instances

Element with field structure and ordered relation

Type of Element with ordered field structure

Module Type OrderedFieldElementType <: FieldElementType <: OrderedRingElementType.
  Include FieldElementType.

  Parameter Alt Ale : A -> A -> Prop.

  Infix "<" := Alt : A_scope.
  Infix "<=" := Ale : A_scope.

  Axiom Order : Order Alt Ale.

  Axiom OrderedARing : OrderedARing Aadd Azero Aopp Amul Aone Alt Ale.
  #[export] Existing Instance OrderedARing.

  Axiom OrderedAField : OrderedField Aadd Azero Aopp Amul Aone Ainv Alt Ale.
  #[export] Existing Instance OrderedAField.

  Notation "| a |" := (Aabs a) : A_scope.
End OrderedFieldElementType.

Instances

Element with field structure and ordered relation and normed

Type of Element with normed ordered field structure

Module Type NormedOrderedFieldElementType <: OrderedFieldElementType.
  Include OrderedFieldElementType.
  Import Reals.

  Parameter a2r : A -> R.
  Axiom A2R : A2R Aadd Azero Aopp Amul Aone Ainv Alt Ale a2r.
  #[export] Existing Instance A2R.
End NormedOrderedFieldElementType.