proposition: Theorem compiler_sound : compiled_sound.
proof: Proof. Proof using HPQ Hilen Hicomp. intros i1 v1 i2 v2 w1. change i1 with (fst (i1,v1)) at 2; change v1 with (snd (i1,v1)) at 1. change i2 with (fst (i2,v2)) at 2; change v2 with (snd (i2,v2)) at 2. generalize (i1,v1) (i2,v2); clear i1 v1 i2 v2. intros st1 st2 (H1 & q & H2); revert H2 w1 H1. induction 1 as [ (i1,v1) | q (i1,v1) (i2,v2) st3 H1 H2 IH2]; simpl; intros w1 H0. + exists w1; split; auto; exists 0; constructor. + destruct H1 as (k & l & I & r & v' & G1 & G2 & G3). inversion G2; subst v' i1; clear G2. destruct (Hicomp linker) with (1 := G3) (3 := H0) as (w2 & G4 & G5). * rewrite Hilen; apply HPQ; subst; exists l, r; auto. * destruct (IH2 _ G5) as (w3 & G6 & G7). exists w3; split; auto. apply sss_compute_trans with (2 := G7); simpl. apply sss_progress_compute. revert G4; apply subcode_sss_progress. apply HPQ; subst; exists l, r; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW.Utils(utils) Undecidability.Shared.Libs.DLW.Code(subcode sss compiler)