From 9a6e3fe764dc2543dfa94de20fe5eec42d6be705 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sat, 29 Nov 2003 17:28:49 +0000 Subject: Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/IntMap/Mapc.v | 673 ++++++++++++++++++++++++++++--------------------- 1 file changed, 379 insertions(+), 294 deletions(-) (limited to 'theories/IntMap/Mapc.v') diff --git a/theories/IntMap/Mapc.v b/theories/IntMap/Mapc.v index b7cede9440..8420ba381a 100644 --- a/theories/IntMap/Mapc.v +++ b/theories/IntMap/Mapc.v @@ -7,451 +7,536 @@ (***********************************************************************) (*i $Id$ 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. +Require Import Bool. +Require Import Sumbool. +Require Import Arith. +Require Import ZArith. +Require Import Addr. +Require Import Adist. +Require Import Addec. +Require Import Map. +Require Import Mapaxioms. +Require Import Fset. +Require Import Mapiter. +Require Import Mapsubset. +Require Import List. +Require Import Lsort. +Require Import Mapcard. +Require Import Mapcanon. Section MapC. - Variable A, B, C : Set. + Variables 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)). + Lemma MapPut_as_Merge_c : + forall m:Map A, + mapcanon A m -> + forall (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. + 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). + Lemma MapPut_behind_as_Merge_c : + forall m:Map A, + mapcanon A m -> + forall (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. + 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. + Lemma MapMerge_empty_m_c : forall m:Map A, MapMerge A (M0 A) m = m. Proof. - Trivial. + 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'')). + Lemma MapMerge_assoc_c : + forall 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. + 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. + Lemma MapMerge_idempotent_c : + forall m:Map A, mapcanon A m -> MapMerge A m m = m. Proof. - Intros. Apply mapcanon_unique. (Apply MapMerge_canon; Assumption). - Assumption. - Apply MapMerge_idempotent. + 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'')). + Lemma MapMerge_RestrTo_l_c : + forall 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. + 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)). + Lemma MapRemove_as_RestrBy_c : + forall m:Map A, + mapcanon A m -> + forall (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. + 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'')). + Lemma MapDomRestrTo_assoc_c : + forall (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. + 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. + Lemma MapDomRestrTo_idempotent_c : + forall 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. + 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')). + Lemma MapDomRestrTo_Dom_c : + forall (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. + 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')). + Lemma MapDomRestrBy_Dom_c : + forall (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. + 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'')). + Lemma MapDomRestrBy_By_c : + forall (m:Map A) (m' 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. + 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'). + Lemma MapDomRestrBy_By_comm_c : + forall (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. + 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'')). + Lemma MapDomRestrBy_To_c : + forall (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. + 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'). + Lemma MapDomRestrBy_To_comm_c : + forall (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. + 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')). + Lemma MapDomRestrTo_By_c : + forall (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. + 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'). + Lemma MapDomRestrTo_By_comm_c : + forall (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. + 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'). + Lemma MapDomRestrTo_To_comm_c : + forall (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. + 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'')). + Lemma MapMerge_DomRestrTo_c : + forall (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. + 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'')). + Lemma MapMerge_DomRestrBy_c : + forall (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. + 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). + Lemma MapDelta_nilpotent_c : + forall 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. + 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)). + Lemma MapDelta_as_Merge_c : + forall 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. + 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')). + Lemma MapDelta_as_DomRestrBy_c : + forall 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. + 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)). + Lemma MapDelta_as_DomRestrBy_2_c : + forall 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. + 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). + Lemma MapDelta_sym_c : + forall 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. + 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')). + Lemma MapDom_Split_1_c : + forall (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. + 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')). + Lemma MapDom_Split_2_c : + forall (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. + 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). + Lemma MapDom_Split_3_c : + forall (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. + 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. + Lemma Map_of_alist_of_Map_c : + forall 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. + 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. + Lemma alist_of_Map_of_alist_c : + forall 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. + 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'). + Lemma MapSubset_antisym_c : + forall (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). + 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'. + Lemma FSubset_antisym_c : + forall 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. + 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). + Lemma MapDisjoint_empty_c : + forall 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. + 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'). + Lemma MapDelta_disjoint_c : + forall 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. + 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'')). +Lemma FSetDelta_assoc_c : + forall 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. + 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'. +Lemma FSet_ext_c : + forall s s':FSet, + mapcanon unit s -> + mapcanon unit s' -> (forall a:ad, in_FSet a s = in_FSet a s') -> s = s'. Proof. - Intros. (Apply (mapcanon_unique unit); Try Assumption). Apply FSet_ext. Assumption. + 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). +Lemma FSetUnion_comm_c : + forall 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. + intros. + apply (mapcanon_unique unit); + try (unfold FSetUnion in |- *; 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'')). +Lemma FSetUnion_assoc_c : + forall 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). + exact (MapMerge_assoc_c unit). Qed. -Lemma FSetUnion_M0_s_c : (s:FSet) (FSetUnion (M0 unit) s)=s. +Lemma FSetUnion_M0_s_c : forall s:FSet, FSetUnion (M0 unit) s = s. Proof. - Exact (MapMerge_empty_m_c unit). + exact (MapMerge_empty_m_c unit). Qed. -Lemma FSetUnion_s_M0_c : (s:FSet) (FSetUnion s (M0 unit))=s. +Lemma FSetUnion_s_M0_c : forall s:FSet, FSetUnion s (M0 unit) = s. Proof. - Exact (MapMerge_m_empty_1 unit). + exact (MapMerge_m_empty_1 unit). Qed. -Lemma FSetUnion_idempotent : (s:FSet) (mapcanon unit s) -> (FSetUnion s s)=s. +Lemma FSetUnion_idempotent : + forall s:FSet, mapcanon unit s -> FSetUnion s s = s. Proof. - Exact (MapMerge_idempotent_c unit). + 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). +Lemma FSetInter_comm_c : + forall 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. + intros. + apply (mapcanon_unique unit); + try (unfold FSetInter in |- *; 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'')). +Lemma FSetInter_assoc_c : + forall 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). + exact (MapDomRestrTo_assoc_c unit unit unit). Qed. -Lemma FSetInter_M0_s_c : (s:FSet) (FSetInter (M0 unit) s)=(M0 unit). +Lemma FSetInter_M0_s_c : forall s:FSet, FSetInter (M0 unit) s = M0 unit. Proof. - Trivial. + trivial. Qed. -Lemma FSetInter_s_M0_c : (s:FSet) (FSetInter s (M0 unit))=(M0 unit). +Lemma FSetInter_s_M0_c : forall s:FSet, FSetInter s (M0 unit) = M0 unit. Proof. - Exact (MapDomRestrTo_m_empty_1 unit unit). + exact (MapDomRestrTo_m_empty_1 unit unit). Qed. -Lemma FSetInter_idempotent : (s:FSet) (mapcanon unit s) -> (FSetInter s s)=s. +Lemma FSetInter_idempotent : + forall s:FSet, mapcanon unit s -> FSetInter s s = s. Proof. - Exact (MapDomRestrTo_idempotent_c unit). + 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'')). +Lemma FSetUnion_Inter_l_c : + forall 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. + intros. apply (mapcanon_unique unit). unfold FSetUnion in |- *. apply MapMerge_canon; try assumption. + unfold FSetInter in |- *. apply MapDomRestrTo_canon; assumption. + unfold FSetInter in |- *; unfold FSetUnion in |- *; + 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'')). +Lemma FSetUnion_Inter_r : + forall 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. + intros. apply (mapcanon_unique unit). unfold FSetUnion in |- *. apply MapMerge_canon; try assumption. + unfold FSetInter in |- *. apply MapDomRestrTo_canon; assumption. + unfold FSetInter in |- *; unfold FSetUnion in |- *; + 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'')). +Lemma FSetInter_Union_l_c : + forall 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. + intros. apply (mapcanon_unique unit). unfold FSetInter in |- *. + apply MapDomRestrTo_canon; try assumption. unfold FSetUnion in |- *. + apply MapMerge_canon; assumption. + unfold FSetUnion in |- *; unfold FSetInter in |- *; 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'')). +Lemma FSetInter_Union_r : + forall 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. + intros. apply (mapcanon_unique unit). unfold FSetInter in |- *. + apply MapDomRestrTo_canon; try assumption. + unfold FSetUnion in |- *. apply MapMerge_canon; unfold FSetInter in |- *; apply MapDomRestrTo_canon; + assumption. + apply FSetInter_Union_r. +Qed. \ No newline at end of file -- cgit v1.2.3