FinMatrix.CoqExt.ElementType

Require Export Hierarchy.

ElementType

One type with decidable equality and zero element

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

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

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

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

An extended `ElementType` equipped with order relation

Module Type OrderedElementType <: ElementType.
  Include ElementType.

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

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

  Axiom Order : Order Alt Ale.
End OrderedElementType.

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

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

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

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

  Include (ElementTypeFun I O).
  Open Scope A_scope.

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

  Infix "+" := Aadd : A_scope.

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

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

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

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

  #[export] Instance Aadd_AMonoid : AMonoid Aadd Azero.
  Proof.
    intros. constructor; intros; autounfold with tA.
    intros. constructor; intros; autounfold with tA.
    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.

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

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

  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.

SRing structure can be derived from the context

Axiom SRing : SRing Aadd 0 Amul 1.
#[export] Existing Instance SRing.

Ring structure can be derived from the context

Axiom ARing : ARing Aadd 0 Aopp Amul 1.
#[export] Existing Instance ARing.

End RingElementType.

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

  Include (MonoidElementTypeFun I O).

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

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

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

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

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

  Parameter Alt Ale : tA -> tA -> 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.

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

  Parameter Ainv : tA -> tA.

  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.

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

  Parameter Alt Ale : tA -> tA -> 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.