proposition: Lemma put_unique: forall (p: PProg)(h: list Label)(s: State)(l l': Label), (step_star (init p) h s /\ In l h /\ In l' h /\ label_is_put l /\ label_is_put l' /\ label_node l = label_node l' /\ label_clock l = label_clock l') -> l = l'.
proof: Proof. intros. open_conjs. assert (L := in_exec h (init p) s l (conj H H0)). destruct L as [h1 [s1 [s2 [h2 [L1 [L2 [L3 L4]]]]]]]. assert (L' := in_exec h (init p) s l' (conj H H1)). destruct L' as [h1' [s1' [s2' [h2' [L1' [L2' [L3' L4']]]]]]]. rewrite L1 in H1. apply in_app_iff in H1. destruct H1 as [H1 | H1]. exfalso. assert (E := in_exec h1 (init p) s1 l' (conj L2 H1)). destruct E as [h1'' [s1'' [s2'' [h2'' [E1 [E2 [E3 E4]]]]]]]. assert (F: step_star s1'' ((l' :: h2'') ++ [l]) s2). apply step_star_app. exists s1. split. apply step_star_end. exists s2''. split; assumption. apply step_star_one. assumption. assert (L := put_inc_clock h2'' s1'' s2 l' l). depremise L. split_all. assumption. assumption. assumption. symmetry. assumption. rewrite H5 in *. apply Nat.lt_irrefl in L. assumption. apply in_inv in H1. destruct H1 as [H1 | H1]. assumption. exfalso. assert (E := in_exec h2 s2 s l' (conj L4 H1)). destruct E as [h1'' [s1'' [s2'' [h2'' [E1 [E2 [E3 E4]]]]]]]. assert (F: step_star s1 ((l :: h1'') ++ [l']) s2''). apply step_star_app. exists s1''. split. apply step_star_end. exists s2. split; assumption. apply step_star_one. assumption. assert (L := put_inc_clock h1'' s1 s2'' l l'). depremise L. split_all. assumption. assumption. assumption. assumption. rewrite H5 in *. apply Nat.lt_irrefl in L. assumption. Qed.
imports: Coq(FunctionalExtensionality Arith Lia) Coq(Arith.Peano_dec Arith.Compare_dec) Coq(Relations.Relation_Operators) Coq(List) Chapar(Predefs)