summaryrefslogtreecommitdiff
path: root/theories7/IntMap/Mapc.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories7/IntMap/Mapc.v')
-rw-r--r--theories7/IntMap/Mapc.v457
1 files changed, 0 insertions, 457 deletions
diff --git a/theories7/IntMap/Mapc.v b/theories7/IntMap/Mapc.v
deleted file mode 100644
index 181050b1..00000000
--- a/theories7/IntMap/Mapc.v
+++ /dev/null
@@ -1,457 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-(*i $Id: Mapc.v,v 1.1.2.1 2004/07/16 19:31:28 herbelin Exp $ i*)
-
-Require Bool.
-Require Sumbool.
-Require Arith.
-Require ZArith.
-Require Addr.
-Require Adist.
-Require Addec.
-Require Map.
-Require Mapaxioms.
-Require Fset.
-Require Mapiter.
-Require Mapsubset.
-Require PolyList.
-Require Lsort.
-Require Mapcard.
-Require Mapcanon.
-
-Section MapC.
-
- Variable A, B, C : Set.
-
- Lemma MapPut_as_Merge_c : (m:(Map A)) (mapcanon A m) ->
- (a:ad) (y:A) (MapPut A m a y)=(MapMerge A m (M1 A a y)).
- Proof.
- Intros. Apply mapcanon_unique. Exact (MapPut_canon A m H a y).
- Apply MapMerge_canon. Assumption.
- Apply M1_canon.
- Apply MapPut_as_Merge.
- Qed.
-
- Lemma MapPut_behind_as_Merge_c : (m:(Map A)) (mapcanon A m) ->
- (a:ad) (y:A) (MapPut_behind A m a y)=(MapMerge A (M1 A a y) m).
- Proof.
- Intros. Apply mapcanon_unique. Exact (MapPut_behind_canon A m H a y).
- Apply MapMerge_canon. Apply M1_canon.
- Assumption.
- Apply MapPut_behind_as_Merge.
- Qed.
-
- Lemma MapMerge_empty_m_c : (m:(Map A)) (MapMerge A (M0 A) m)=m.
- Proof.
- Trivial.
- Qed.
-
- Lemma MapMerge_assoc_c : (m,m',m'':(Map A))
- (mapcanon A m) -> (mapcanon A m') -> (mapcanon A m'') ->
- (MapMerge A (MapMerge A m m') m'')=(MapMerge A m (MapMerge A m' m'')).
- Proof.
- Intros. Apply mapcanon_unique.
- (Apply MapMerge_canon; Try Assumption). (Apply MapMerge_canon; Try Assumption).
- (Apply MapMerge_canon; Try Assumption). (Apply MapMerge_canon; Try Assumption).
- Apply MapMerge_assoc.
- Qed.
-
- Lemma MapMerge_idempotent_c : (m:(Map A)) (mapcanon A m) -> (MapMerge A m m)=m.
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapMerge_canon; Assumption).
- Assumption.
- Apply MapMerge_idempotent.
- Qed.
-
- Lemma MapMerge_RestrTo_l_c : (m,m',m'':(Map A))
- (mapcanon A m) -> (mapcanon A m'') ->
- (MapMerge A (MapDomRestrTo A A m m') m'')=
- (MapDomRestrTo A A (MapMerge A m m'') (MapMerge A m' m'')).
- Proof.
- Intros. Apply mapcanon_unique. Apply MapMerge_canon. Apply MapDomRestrTo_canon; Assumption.
- Assumption.
- Apply MapDomRestrTo_canon; Apply MapMerge_canon; Assumption.
- Apply MapMerge_RestrTo_l.
- Qed.
-
- Lemma MapRemove_as_RestrBy_c : (m:(Map A)) (mapcanon A m) ->
- (a:ad) (y:B) (MapRemove A m a)=(MapDomRestrBy A B m (M1 B a y)).
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapRemove_canon; Assumption).
- (Apply MapDomRestrBy_canon; Assumption).
- Apply MapRemove_as_RestrBy.
- Qed.
-
- Lemma MapDomRestrTo_assoc_c : (m:(Map A)) (m':(Map B)) (m'':(Map C))
- (mapcanon A m) ->
- (MapDomRestrTo A C (MapDomRestrTo A B m m') m'')=
- (MapDomRestrTo A B m (MapDomRestrTo B C m' m'')).
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapDomRestrTo_canon; Try Assumption).
- (Apply MapDomRestrTo_canon; Try Assumption).
- (Apply MapDomRestrTo_canon; Try Assumption).
- Apply MapDomRestrTo_assoc.
- Qed.
-
- Lemma MapDomRestrTo_idempotent_c : (m:(Map A)) (mapcanon A m) ->
- (MapDomRestrTo A A m m)=m.
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapDomRestrTo_canon; Assumption).
- Assumption.
- Apply MapDomRestrTo_idempotent.
- Qed.
-
- Lemma MapDomRestrTo_Dom_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
- (MapDomRestrTo A B m m')=(MapDomRestrTo A unit m (MapDom B m')).
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapDomRestrTo_canon; Assumption).
- (Apply MapDomRestrTo_canon; Assumption).
- Apply MapDomRestrTo_Dom.
- Qed.
-
- Lemma MapDomRestrBy_Dom_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
- (MapDomRestrBy A B m m')=(MapDomRestrBy A unit m (MapDom B m')).
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon; Assumption.
- Apply MapDomRestrBy_canon; Assumption.
- Apply MapDomRestrBy_Dom.
- Qed.
-
- Lemma MapDomRestrBy_By_c : (m:(Map A)) (m':(Map B)) (m'':(Map B))
- (mapcanon A m) ->
- (MapDomRestrBy A B (MapDomRestrBy A B m m') m'')=
- (MapDomRestrBy A B m (MapMerge B m' m'')).
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapDomRestrBy_canon; Try Assumption).
- (Apply MapDomRestrBy_canon; Try Assumption).
- (Apply MapDomRestrBy_canon; Try Assumption).
- Apply MapDomRestrBy_By.
- Qed.
-
- Lemma MapDomRestrBy_By_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C))
- (mapcanon A m) ->
- (MapDomRestrBy A C (MapDomRestrBy A B m m') m'')=
- (MapDomRestrBy A B (MapDomRestrBy A C m m'') m').
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon.
- (Apply MapDomRestrBy_canon; Assumption).
- Apply MapDomRestrBy_canon. (Apply MapDomRestrBy_canon; Assumption).
- Apply MapDomRestrBy_By_comm.
- Qed.
-
- Lemma MapDomRestrBy_To_c : (m:(Map A)) (m':(Map B)) (m'':(Map C))
- (mapcanon A m) ->
- (MapDomRestrBy A C (MapDomRestrTo A B m m') m'')=
- (MapDomRestrTo A B m (MapDomRestrBy B C m' m'')).
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon.
- (Apply MapDomRestrTo_canon; Assumption).
- (Apply MapDomRestrTo_canon; Assumption).
- Apply MapDomRestrBy_To.
- Qed.
-
- Lemma MapDomRestrBy_To_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C))
- (mapcanon A m) ->
- (MapDomRestrBy A C (MapDomRestrTo A B m m') m'')=
- (MapDomRestrTo A B (MapDomRestrBy A C m m'') m').
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon.
- Apply MapDomRestrTo_canon; Assumption.
- Apply MapDomRestrTo_canon. Apply MapDomRestrBy_canon; Assumption.
- Apply MapDomRestrBy_To_comm.
- Qed.
-
- Lemma MapDomRestrTo_By_c : (m:(Map A)) (m':(Map B)) (m'':(Map C))
- (mapcanon A m) ->
- (MapDomRestrTo A C (MapDomRestrBy A B m m') m'')=
- (MapDomRestrTo A C m (MapDomRestrBy C B m'' m')).
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
- Apply MapDomRestrBy_canon; Assumption.
- Apply MapDomRestrTo_canon; Assumption.
- Apply MapDomRestrTo_By.
- Qed.
-
- Lemma MapDomRestrTo_By_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C))
- (mapcanon A m) ->
- (MapDomRestrTo A C (MapDomRestrBy A B m m') m'')=
- (MapDomRestrBy A B (MapDomRestrTo A C m m'') m').
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
- (Apply MapDomRestrBy_canon; Assumption).
- Apply MapDomRestrBy_canon. (Apply MapDomRestrTo_canon; Assumption).
- Apply MapDomRestrTo_By_comm.
- Qed.
-
- Lemma MapDomRestrTo_To_comm_c : (m:(Map A)) (m':(Map B)) (m'':(Map C))
- (mapcanon A m) ->
- (MapDomRestrTo A C (MapDomRestrTo A B m m') m'')=
- (MapDomRestrTo A B (MapDomRestrTo A C m m'') m').
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
- Apply MapDomRestrTo_canon; Assumption.
- Apply MapDomRestrTo_canon. Apply MapDomRestrTo_canon; Assumption.
- Apply MapDomRestrTo_To_comm.
- Qed.
-
- Lemma MapMerge_DomRestrTo_c : (m,m':(Map A)) (m'':(Map B))
- (mapcanon A m) -> (mapcanon A m') ->
- (MapDomRestrTo A B (MapMerge A m m') m'')=
- (MapMerge A (MapDomRestrTo A B m m'') (MapDomRestrTo A B m' m'')).
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
- (Apply MapMerge_canon; Assumption).
- Apply MapMerge_canon. (Apply MapDomRestrTo_canon; Assumption).
- (Apply MapDomRestrTo_canon; Assumption).
- Apply MapMerge_DomRestrTo.
- Qed.
-
- Lemma MapMerge_DomRestrBy_c : (m,m':(Map A)) (m'':(Map B))
- (mapcanon A m) -> (mapcanon A m') ->
- (MapDomRestrBy A B (MapMerge A m m') m'')=
- (MapMerge A (MapDomRestrBy A B m m'') (MapDomRestrBy A B m' m'')).
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDomRestrBy_canon. Apply MapMerge_canon; Assumption.
- Apply MapMerge_canon. Apply MapDomRestrBy_canon; Assumption.
- Apply MapDomRestrBy_canon; Assumption.
- Apply MapMerge_DomRestrBy.
- Qed.
-
- Lemma MapDelta_nilpotent_c : (m:(Map A)) (mapcanon A m) ->
- (MapDelta A m m)=(M0 A).
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
- Apply M0_canon.
- Apply MapDelta_nilpotent.
- Qed.
-
- Lemma MapDelta_as_Merge_c : (m,m':(Map A))
- (mapcanon A m) -> (mapcanon A m') ->
- (MapDelta A m m')=
- (MapMerge A (MapDomRestrBy A A m m') (MapDomRestrBy A A m' m)).
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
- (Apply MapMerge_canon; Apply MapDomRestrBy_canon; Assumption).
- Apply MapDelta_as_Merge.
- Qed.
-
- Lemma MapDelta_as_DomRestrBy_c : (m,m':(Map A))
- (mapcanon A m) -> (mapcanon A m') ->
- (MapDelta A m m')=
- (MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m m')).
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDelta_canon; Assumption.
- Apply MapDomRestrBy_canon. (Apply MapMerge_canon; Assumption).
- Apply MapDelta_as_DomRestrBy.
- Qed.
-
- Lemma MapDelta_as_DomRestrBy_2_c : (m,m':(Map A))
- (mapcanon A m) -> (mapcanon A m') ->
- (MapDelta A m m')=
- (MapDomRestrBy A A (MapMerge A m m') (MapDomRestrTo A A m' m)).
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
- Apply MapDomRestrBy_canon. Apply MapMerge_canon; Assumption.
- Apply MapDelta_as_DomRestrBy_2.
- Qed.
-
- Lemma MapDelta_sym_c : (m,m':(Map A))
- (mapcanon A m) -> (mapcanon A m') -> (MapDelta A m m')=(MapDelta A m' m).
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
- (Apply MapDelta_canon; Assumption). Apply MapDelta_sym.
- Qed.
-
- Lemma MapDom_Split_1_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
- m=(MapMerge A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m')).
- Proof.
- Intros. Apply mapcanon_unique. Assumption.
- Apply MapMerge_canon. Apply MapDomRestrTo_canon; Assumption.
- Apply MapDomRestrBy_canon; Assumption.
- Apply MapDom_Split_1.
- Qed.
-
- Lemma MapDom_Split_2_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
- m=(MapMerge A (MapDomRestrBy A B m m') (MapDomRestrTo A B m m')).
- Proof.
- Intros. Apply mapcanon_unique. Assumption.
- Apply MapMerge_canon. (Apply MapDomRestrBy_canon; Assumption).
- (Apply MapDomRestrTo_canon; Assumption).
- Apply MapDom_Split_2.
- Qed.
-
- Lemma MapDom_Split_3_c : (m:(Map A)) (m':(Map B)) (mapcanon A m) ->
- (MapDomRestrTo A A (MapDomRestrTo A B m m') (MapDomRestrBy A B m m'))=
- (M0 A).
- Proof.
- Intros. Apply mapcanon_unique. Apply MapDomRestrTo_canon.
- Apply MapDomRestrTo_canon; Assumption.
- Apply M0_canon.
- Apply MapDom_Split_3.
- Qed.
-
- Lemma Map_of_alist_of_Map_c : (m:(Map A)) (mapcanon A m) ->
- (Map_of_alist A (alist_of_Map A m))=m.
- Proof.
- Intros. (Apply mapcanon_unique; Try Assumption). Apply Map_of_alist_canon.
- Apply Map_of_alist_of_Map.
- Qed.
-
- Lemma alist_of_Map_of_alist_c : (l:(alist A)) (alist_sorted_2 A l) ->
- (alist_of_Map A (Map_of_alist A l))=l.
- Proof.
- Intros. Apply alist_canonical. Apply alist_of_Map_of_alist.
- Apply alist_of_Map_sorts2.
- Assumption.
- Qed.
-
- Lemma MapSubset_antisym_c : (m:(Map A)) (m':(Map B))
- (mapcanon A m) -> (mapcanon B m') ->
- (MapSubset A B m m') -> (MapSubset B A m' m) -> (MapDom A m)=(MapDom B m').
- Proof.
- Intros. Apply (mapcanon_unique unit). (Apply MapDom_canon; Assumption).
- (Apply MapDom_canon; Assumption).
- (Apply MapSubset_antisym; Assumption).
- Qed.
-
- Lemma FSubset_antisym_c : (s,s':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
- (MapSubset ? ? s s') -> (MapSubset ? ? s' s) -> s=s'.
- Proof.
- Intros. Apply (mapcanon_unique unit); Try Assumption. Apply FSubset_antisym; Assumption.
- Qed.
-
- Lemma MapDisjoint_empty_c : (m:(Map A)) (mapcanon A m) ->
- (MapDisjoint A A m m) -> m=(M0 A).
- Proof.
- Intros. Apply mapcanon_unique; Try Assumption; Try Apply M0_canon.
- Apply MapDisjoint_empty; Assumption.
- Qed.
-
- Lemma MapDelta_disjoint_c : (m,m':(Map A)) (mapcanon A m) -> (mapcanon A m') ->
- (MapDisjoint A A m m') -> (MapDelta A m m')=(MapMerge A m m').
- Proof.
- Intros. Apply mapcanon_unique. (Apply MapDelta_canon; Assumption).
- (Apply MapMerge_canon; Assumption). Apply MapDelta_disjoint; Assumption.
- Qed.
-
-End MapC.
-
-Lemma FSetDelta_assoc_c : (s,s',s'':FSet)
- (mapcanon unit s) -> (mapcanon unit s') -> (mapcanon unit s'') ->
- (MapDelta ? (MapDelta ? s s') s'')=(MapDelta ? s (MapDelta ? s' s'')).
-Proof.
- Intros. Apply (mapcanon_unique unit). Apply MapDelta_canon. (Apply MapDelta_canon; Assumption).
- Assumption.
- Apply MapDelta_canon. Assumption.
- (Apply MapDelta_canon; Assumption).
- Apply FSetDelta_assoc; Assumption.
-Qed.
-
-Lemma FSet_ext_c : (s,s':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
- ((a:ad) (in_FSet a s)=(in_FSet a s')) -> s=s'.
-Proof.
- Intros. (Apply (mapcanon_unique unit); Try Assumption). Apply FSet_ext. Assumption.
-Qed.
-
-Lemma FSetUnion_comm_c : (s,s':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
- (FSetUnion s s')=(FSetUnion s' s).
-Proof.
- Intros.
- Apply (mapcanon_unique unit); Try (Unfold FSetUnion; Apply MapMerge_canon; Assumption).
- Apply FSetUnion_comm.
-Qed.
-
-Lemma FSetUnion_assoc_c : (s,s',s'':FSet)
- (mapcanon unit s) -> (mapcanon unit s') -> (mapcanon unit s'') ->
- (FSetUnion (FSetUnion s s') s'')=(FSetUnion s (FSetUnion s' s'')).
-Proof.
- Exact (MapMerge_assoc_c unit).
-Qed.
-
-Lemma FSetUnion_M0_s_c : (s:FSet) (FSetUnion (M0 unit) s)=s.
-Proof.
- Exact (MapMerge_empty_m_c unit).
-Qed.
-
-Lemma FSetUnion_s_M0_c : (s:FSet) (FSetUnion s (M0 unit))=s.
-Proof.
- Exact (MapMerge_m_empty_1 unit).
-Qed.
-
-Lemma FSetUnion_idempotent : (s:FSet) (mapcanon unit s) -> (FSetUnion s s)=s.
-Proof.
- Exact (MapMerge_idempotent_c unit).
-Qed.
-
-Lemma FSetInter_comm_c : (s,s':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
- (FSetInter s s')=(FSetInter s' s).
-Proof.
- Intros.
- Apply (mapcanon_unique unit); Try (Unfold FSetInter; Apply MapDomRestrTo_canon; Assumption).
- Apply FSetInter_comm.
-Qed.
-
-Lemma FSetInter_assoc_c : (s,s',s'':FSet)
- (mapcanon unit s) ->
- (FSetInter (FSetInter s s') s'')=(FSetInter s (FSetInter s' s'')).
-Proof.
- Exact (MapDomRestrTo_assoc_c unit unit unit).
-Qed.
-
-Lemma FSetInter_M0_s_c : (s:FSet) (FSetInter (M0 unit) s)=(M0 unit).
-Proof.
- Trivial.
-Qed.
-
-Lemma FSetInter_s_M0_c : (s:FSet) (FSetInter s (M0 unit))=(M0 unit).
-Proof.
- Exact (MapDomRestrTo_m_empty_1 unit unit).
-Qed.
-
-Lemma FSetInter_idempotent : (s:FSet) (mapcanon unit s) -> (FSetInter s s)=s.
-Proof.
- Exact (MapDomRestrTo_idempotent_c unit).
-Qed.
-
-Lemma FSetUnion_Inter_l_c : (s,s',s'':FSet) (mapcanon unit s) -> (mapcanon unit s'') ->
- (FSetUnion (FSetInter s s') s'')=(FSetInter (FSetUnion s s'') (FSetUnion s' s'')).
-Proof.
- Intros. Apply (mapcanon_unique unit). Unfold FSetUnion. (Apply MapMerge_canon; Try Assumption).
- Unfold FSetInter. (Apply MapDomRestrTo_canon; Assumption).
- Unfold FSetInter; Unfold FSetUnion; Apply MapDomRestrTo_canon; Apply MapMerge_canon; Assumption.
- Apply FSetUnion_Inter_l.
-Qed.
-
-Lemma FSetUnion_Inter_r : (s,s',s'':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
- (FSetUnion s (FSetInter s' s''))=(FSetInter (FSetUnion s s') (FSetUnion s s'')).
-Proof.
- Intros. Apply (mapcanon_unique unit). Unfold FSetUnion. (Apply MapMerge_canon; Try Assumption).
- Unfold FSetInter. (Apply MapDomRestrTo_canon; Assumption).
- Unfold FSetInter; Unfold FSetUnion; Apply MapDomRestrTo_canon; Apply MapMerge_canon; Assumption.
- Apply FSetUnion_Inter_r.
-Qed.
-
-Lemma FSetInter_Union_l_c : (s,s',s'':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
- (FSetInter (FSetUnion s s') s'')=(FSetUnion (FSetInter s s'') (FSetInter s' s'')).
-Proof.
- Intros. Apply (mapcanon_unique unit). Unfold FSetInter.
- Apply MapDomRestrTo_canon; Try Assumption. Unfold FSetUnion.
- Apply MapMerge_canon; Assumption.
- Unfold FSetUnion; Unfold FSetInter; Apply MapMerge_canon; Apply MapDomRestrTo_canon;
- Assumption.
- Apply FSetInter_Union_l.
-Qed.
-
-Lemma FSetInter_Union_r : (s,s',s'':FSet) (mapcanon unit s) -> (mapcanon unit s') ->
- (FSetInter s (FSetUnion s' s''))=(FSetUnion (FSetInter s s') (FSetInter s s'')).
-Proof.
- Intros. Apply (mapcanon_unique unit). Unfold FSetInter.
- Apply MapDomRestrTo_canon; Try Assumption.
- Unfold FSetUnion. Apply MapMerge_canon; Unfold FSetInter; Apply MapDomRestrTo_canon; Assumption.
- Apply FSetInter_Union_r.
-Qed.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 16:28:19 +0000