X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofToStrong.v;h=0d90d4c6c128d6f58f3e74b46ae4c5c0457b1ec3;hp=2ea0c4a1e4cfaea4311bcda04a7090166d87d53f;hb=af41ffb1692ae207554342ccdc3bf73abaa75a01;hpb=16fef762b0a81544a31b6392059d148431e984be diff --git a/src/HaskProofToStrong.v b/src/HaskProofToStrong.v index 2ea0c4a..0d90d4c 100644 --- a/src/HaskProofToStrong.v +++ b/src/HaskProofToStrong.v @@ -763,11 +763,9 @@ Section HaskProofToStrong. | RAppCo Γ Δ Σ κ σ₁ σ₂ γ σ l => let case_RAppCo := tt in _ | RAbsCo Γ Δ Σ κ σ σ₁ σ₂ y => let case_RAbsCo := tt in _ | RApp Γ Δ Σ₁ Σ₂ tx te p => let case_RApp := tt in _ - | RLet Γ Δ Σ₁ Σ₂ σ₁ σ₂ p => let case_RLet := tt in _ - | RCut Γ Δ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ + | RCut Γ Δ Σ Σ₁ Σ₁₂ Σ₂ Σ₃ l => let case_RCut := tt in _ | RLeft Γ Δ Σ₁ Σ₂ Σ l => let case_RLeft := tt in _ | RRight Γ Δ Σ₁ Σ₂ Σ l => let case_RRight := tt in _ - | RWhere Γ Δ Σ₁ Σ₂ Σ₃ σ₁ σ₂ p => let case_RWhere := tt in _ | RVoid _ _ l => let case_RVoid := tt in _ | RBrak Σ a b c n m => let case_RBrak := tt in _ | REsc Σ a b c n m => let case_REsc := tt in _ @@ -869,54 +867,19 @@ Section HaskProofToStrong. simpl in *. apply (EApp _ _ _ _ _ _ q1' q2'). - destruct case_RLet. - eapply rlet. - apply X_. - - destruct case_RWhere. - apply ILeaf. - simpl in *; intros. - destruct vars; try destruct o; inversion H. - destruct vars2; try destruct o; inversion H2. - clear H2. - - assert ((Σ₁,,Σ₃) = mapOptionTree ξ (vars1,,vars2_2)) as H13; simpl; subst; auto. - refine (fresh_lemma _ ξ _ _ σ₁ p H13 >>>= (fun pf => _)). - apply FreshMon. - - destruct pf as [ vnew [ pf1 pf2 ]]. - set (update_xi ξ p (((vnew, σ₁ )) :: nil)) as ξ' in *. - inversion X_. - apply ileaf in X. - apply ileaf in X0. - simpl in *. - - refine (X ξ' (vars1,,([vnew],,vars2_2)) _ >>>= fun X0' => _). - apply FreshMon. - simpl. - inversion pf1. - rewrite H3. - rewrite H4. - rewrite pf2. - reflexivity. - - refine (X0 ξ vars2_1 _ >>>= fun X1' => _). - apply FreshMon. - reflexivity. - apply FreshMon. - - apply ILeaf. - apply ileaf in X0'. - apply ileaf in X1'. - simpl in *. - apply ELet with (ev:=vnew)(tv:=σ₁). - apply X1'. - apply X0'. - destruct case_RCut. + apply rassoc. + apply swapr. + apply rassoc'. + inversion X_. subst. clear X_. + + apply rassoc' in X0. + apply swapr in X0. + apply rassoc in X0. + induction Σ₃. destruct a. subst.