- 01
- 02
- 03
- 04
- 05
- 06
- 07
- 08
- 09
- 10
- 11
- 12
- 13
- 14
- 15
- 16
- 17
- 18
- 19
- 20
- 21
- 22
- 23
- 24
- 25
- 26
- 27
- 28
- 29
- 30
- 31
- 32
- 33
- 34
- 35
- 36
- 37
- 38
- 39
- 40
- 41
Definition uilv_add_trivial {N} te (t : list TE) (traces : Traces N)
i j (Ht : MInt_ trace_elems_don't_commute j true traces t)
s s' (Hls : LongStep s (te :: t) s')
(Htriv : trivial_add i j traces) :
MInt_ trace_elems_don't_commute i true (push_te traces i te) (te :: t).
Proof with autorewrite with vector; eauto with vector; try vec_forall_eq_contradiction.
unfold push_te.
unfold trivial_add in Htriv.
destruct (Fin.eq_dec i j) as [Hij|Hij].
(* [i=j], solving by constructor: *)
{ subst.
unfold trivial_add.
eapply mint_keep with (rest := traces[@j])...
}
remember traces[@j] as t2_.
destruct t2_ as [|te2 t2]; subst.
{ inversion Ht as [vec Hvec|? ? ? ? ? Hj Hcont|? ? ? ? ? ? Hjj0 Hswitch Hj Hcont];
subst.
- eapply mint_keep with (prog := true)...
eapply mint_nil...
- rewrite Hj in Heqt2_.
discriminate.
}
remember traces[@i] as t1_.
destruct t1_ as [|te1 t1]; subst.
(* [te] is the last element in i-th trace: *)
{ eapply mint_keep with (rest := []) (prog := false)...
inversion Ht as [vec Hvec|? ? ? ? ? Hj Hcont|? ? ? ? ? ? Hjj0 Hswitch Hj Hcont];
subst...
rewrite Heqt1_ in *.
eapply mint_switch...
rewrite <-Heqt1_...
}
destruct Htriv as [|[Hij' Hcomm]]; [contradiction Hij|idtac].
eapply mint_keep with (rest := te1 :: t1) (prog := false)...
rewrite Heqt1_, Vec.replace_id.
inversion Ht as [vec Hvec|? ? ? ? ? Hj Hcont|? ? ? ? ? ? Hjj0 Hswitch Hj Hcont]; subst...
replace te0 with te2 in * by congruence.
eapply mint_switch...
rewrite <-Heqt1_...
Defined.
Follow us!