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.
Generic support for algebraic substructures.
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.
This module may be used through the import of Algebra.Algebra, or
Algebra.Algebra_wDep, where it is exported.
Brief description
Description
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
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.