Library Algebra.Sub_struct

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Generic support for algebraic substructures.

Description

Let T be a type endowed with sone algebraic structure.
Let compatible : (T Prop) Prop be the predicate stating that a subset is closed for the constants and operations involved in the algebraic structure.
  • span (gen : T Prop) is the algebraic span of the subset gen, ie the intersection of all subsets satisfying compatible and containning gen.

Usage

This module may be used through the import of Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

From Requisite Require Import stdlib ssr.

From Subsets Require Import Subsets.

Section Span_Algebraic_Structure.

Context {T : Type}.

Variable compatible : (T Prop) Prop.

Hypothesis compatible_inter_any :
   {Idx : Type} {PT : Idx T Prop},
    ( i, compatible (PT i)) compatible (inter_any PT).

Definition span (gen : T Prop) : T Prop :=
  inter_any (fun (P : { PT | compatible PT incl gen PT }) ⇒ proj1_sig P).

Lemma span_compatible : gen, compatible (span gen).
Proof. intros; apply compatible_inter_any; intros [PT HPT]; easy. Qed.

Lemma span_incl : gen, incl gen (span gen).
Proof. intros; apply inter_any_glb; intros [PT HPT]; easy. Qed.

Lemma span_lub :
   gen PT, compatible PT incl gen PT incl (span gen) PT.
Proof. move=>> HPT1 HPT2 x Hx; apply (Hx (exist2 _ _ _ HPT1 HPT2)). Qed.

Lemma span_full : PT, compatible PT span PT = PT.
Proof.
intros PT HPT; apply subset_ext_equiv; split;
    [apply span_lub; easy | apply span_incl].
Qed.

End Span_Algebraic_Structure.