Changeset 2307 for src/common/PositiveMap.ma

Timestamp:

Aug 30, 2012, 4:47:58 PM (7 years ago)

Author:

campbell

Message:

Half the proofs for sound cost labelling check.

File:

• src/common/PositiveMap.ma (modified) (1 diff)

src/common/PositiveMap.ma

@@ -548 +548 @@
 ] qed.
 
-
-
+lemma pm_try_remove_some' : ∀A,p,t,a.
+  lookup_opt A p t = Some A a →
+  ∃t'. pm_try_remove A p t = Some ? 〈a,t'〉.
+#A #p elim p
+[ * [ #a #L normalize in L; destruct
+    | #q #l #r #a #L normalize in L; destruct % [2: % | skip ]
+    ]
+| #q #IH *
+  [ #a #L normalize in L; destruct
+  | #x #l #r #a #L cases (IH r a L) #r' #R
+    % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ]
+  ]
+| #q #IH *
+  [ #a #L normalize in L; destruct
+  | #x #l #r #a #L cases (IH l a L) #l' #R
+    % [2: whd in ⊢ (??%?); >R in ⊢ (??%?); % | skip ]
+  ]
+] qed.
+
+