From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- common/Subtyping.v | 202 ++++++++++++++++++++++++++--------------------------- 1 file changed, 101 insertions(+), 101 deletions(-) (limited to 'common/Subtyping.v') diff --git a/common/Subtyping.v b/common/Subtyping.v index e1bf61af..c09226e0 100644 --- a/common/Subtyping.v +++ b/common/Subtyping.v @@ -207,7 +207,7 @@ Definition type_move (e: typenv) (r1 r2: positive) : res (bool * typenv) := (** Solve the remaining subtyping constraints by iteration. *) Fixpoint solve_rec (e: typenv) (changed: bool) (q: list constraint) : res (typenv * bool) := - match q with + match q with | nil => OK (e, changed) | (r1, r2) :: q' => @@ -222,7 +222,7 @@ Definition weight_bounds (ob: option bounds) : nat := Lemma weight_bounds_1: forall lo hi s, weight_bounds (Some (B lo hi s)) < weight_bounds None. Proof. - intros; simpl. generalize (T.weight_range hi); omega. + intros; simpl. generalize (T.weight_range hi); omega. Qed. Lemma weight_bounds_2: @@ -230,7 +230,7 @@ Lemma weight_bounds_2: T.sub lo2 lo1 -> T.sub hi1 hi2 -> lo1 <> lo2 \/ hi1 <> hi2 -> weight_bounds (Some (B lo1 hi1 s1)) < weight_bounds (Some (B lo2 hi2 s2)). Proof. - intros; simpl. + intros; simpl. generalize (T.weight_sub _ _ s1) (T.weight_sub _ _ s2) (T.weight_sub _ _ H) (T.weight_sub _ _ H0); intros. destruct H1. assert (T.weight lo2 < T.weight lo1) by (apply T.weight_sub_strict; auto). omega. @@ -245,7 +245,7 @@ Lemma weight_type_move: (e'.(te_sub) = e.(te_sub) \/ e'.(te_sub) = (r1, r2) :: e.(te_sub)) /\ (forall r, weight_bounds e'.(te_typ)!r <= weight_bounds e.(te_typ)!r) /\ (changed = true -> - weight_bounds e'.(te_typ)!r1 + weight_bounds e'.(te_typ)!r2 + weight_bounds e'.(te_typ)!r1 + weight_bounds e'.(te_typ)!r2 < weight_bounds e.(te_typ)!r1 + weight_bounds e.(te_typ)!r2). Proof. unfold type_move; intros. @@ -267,22 +267,22 @@ Local Opaque weight_bounds. + split; auto. split; intros. omega. discriminate. + assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1))) by (apply weight_bounds_2; auto with ty). - split; auto. split; intros. + split; auto. split; intros. rewrite PTree.gsspec. destruct (peq r r1). subst r. rewrite E1. omega. omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. + assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2))) by (apply weight_bounds_2; auto with ty). - split; auto. split; intros. + split; auto. split; intros. rewrite PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. omega. omega. rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. + assert (weight_bounds (Some b1) < weight_bounds (Some (B lo1 hi1 s1))) by (apply weight_bounds_2; auto with ty). assert (weight_bounds (Some b2) < weight_bounds (Some (B lo2 hi2 s2))) by (apply weight_bounds_2; auto with ty). - split; auto. split; intros. + split; auto. split; intros. rewrite ! PTree.gsspec. destruct (peq r r2). subst r. rewrite E2. omega. - destruct (peq r r1). subst r. rewrite E1. omega. + destruct (peq r r1). subst r. rewrite E1. omega. omega. rewrite PTree.gss. rewrite PTree.gso by auto. rewrite PTree.gss. omega. @@ -290,15 +290,15 @@ Local Opaque weight_bounds. assert (weight_bounds (Some b2) < weight_bounds None) by (apply weight_bounds_1). inv H; simpl. split. destruct (T.sub_dec hi1 lo1); auto. - split; intros. + split; intros. rewrite PTree.gsspec. destruct (peq r r2). subst r; rewrite E2; omega. omega. - rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. + rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E1. omega. - set (b1 := B (T.low_bound hi2) hi2 (T.low_bound_sub hi2)) in *. assert (weight_bounds (Some b1) < weight_bounds None) by (apply weight_bounds_1). inv H; simpl. split. destruct (T.sub_dec hi2 lo2); auto. - split; intros. + split; intros. rewrite PTree.gsspec. destruct (peq r r1). subst r; rewrite E1; omega. omega. rewrite PTree.gss. rewrite PTree.gso by auto. rewrite E2. omega. @@ -323,7 +323,7 @@ Lemma weight_solve_rec: <= weight_constraints e.(te_typ) e.(te_sub) + weight_constraints e.(te_typ) q. Proof. induction q; simpl; intros. -- inv H. split. intros; omega. replace (changed' && negb changed') with false. +- inv H. split. intros; omega. replace (changed' && negb changed') with false. omega. destruct changed'; auto. - destruct a as [r1 r2]; monadInv H; simpl. rename x into changed1. rename x0 into e1. @@ -334,7 +334,7 @@ Proof. weight_constraints (te_typ e) (te_sub e)) by (apply weight_constraints_tighter; auto). assert (Q: weight_constraints (te_typ e1) (te_sub e1) <= - weight_constraints (te_typ e1) (te_sub e) + + weight_constraints (te_typ e1) (te_sub e) + weight_bounds (te_typ e1)!r1 + weight_bounds (te_typ e1)!r2). { destruct A as [Q|Q]; rewrite Q. omega. simpl. omega. } assert (R: weight_constraints (te_typ e1) q <= weight_constraints (te_typ e) q) @@ -342,16 +342,16 @@ Proof. set (ch1 := if changed' && negb (changed || changed1) then 1 else 0) in *. set (ch2 := if changed' && negb changed then 1 else 0) in *. destruct changed1. - assert (ch2 <= ch1 + 1). - { unfold ch2, ch1. rewrite orb_true_r. simpl. rewrite andb_false_r. + assert (ch2 <= ch1 + 1). + { unfold ch2, ch1. rewrite orb_true_r. simpl. rewrite andb_false_r. destruct (changed' && negb changed); omega. } exploit C; eauto. omega. assert (ch2 <= ch1). { unfold ch2, ch1. rewrite orb_false_r. omega. } - generalize (B r1) (B r2); omega. + generalize (B r1) (B r2); omega. Qed. -Definition weight_typenv (e: typenv) : nat := +Definition weight_typenv (e: typenv) : nat := weight_constraints e.(te_typ) e.(te_sub). (** Iterative solving of the remaining constraints *) @@ -364,7 +364,7 @@ Function solve_constraints (e: typenv) {measure weight_typenv e}: res typenv := end. Proof. intros. exploit weight_solve_rec; eauto. simpl. intros [A B]. - unfold weight_typenv. omega. + unfold weight_typenv. omega. Qed. Definition typassign := positive -> T.t. @@ -383,7 +383,7 @@ Definition satisf (te: typassign) (e: typenv) : Prop := Lemma satisf_initial: forall te, satisf te initial. Proof. - unfold initial; intros; split; simpl; intros. + unfold initial; intros; split; simpl; intros. rewrite PTree.gempty in H; discriminate. contradiction. Qed. @@ -398,11 +398,11 @@ Proof. destruct (T.eq lo (T.lub lo ty)); monadInv H. subst e'; auto. destruct H0 as [P Q]; split; auto; intros. - destruct (peq x x0). + destruct (peq x x0). + subst x0. rewrite E in H; inv H. - exploit (P x); simpl. rewrite PTree.gss; eauto. intuition. - apply T.sub_trans with (T.lub lo0 ty); auto. eapply T.lub_left; eauto. - + eapply P; simpl. rewrite PTree.gso; eauto. + exploit (P x); simpl. rewrite PTree.gss; eauto. intuition. + apply T.sub_trans with (T.lub lo0 ty); auto. eapply T.lub_left; eauto. + + eapply P; simpl. rewrite PTree.gso; eauto. - inv H. destruct H0 as [P Q]; split; auto; intros. eapply P; simpl. rewrite PTree.gso; eauto. congruence. Qed. @@ -416,12 +416,12 @@ Proof. destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. - destruct (T.sub_dec ty hi); try discriminate. destruct (T.eq lo (T.lub lo ty)); monadInv H. - + subst e'. apply T.sub_trans with lo. + + subst e'. apply T.sub_trans with lo. rewrite e0. eapply T.lub_right; eauto. eapply P; eauto. - + apply T.sub_trans with (T.lub lo ty). - eapply T.lub_right; eauto. - eapply (P x). simpl. rewrite PTree.gss; eauto. -- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto. + + apply T.sub_trans with (T.lub lo ty). + eapply T.lub_right; eauto. + eapply (P x). simpl. rewrite PTree.gss; eauto. +- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto. Qed. Lemma type_defs_incr: @@ -448,11 +448,11 @@ Proof. destruct (T.eq hi (T.glb hi ty)); monadInv H. subst e'; auto. destruct H0 as [P Q]; split; auto; intros. - destruct (peq x x0). + destruct (peq x x0). + subst x0. rewrite E in H; inv H. - exploit (P x); simpl. rewrite PTree.gss; eauto. intuition. - apply T.sub_trans with (T.glb hi0 ty); auto. eapply T.glb_left; eauto. - + eapply P; simpl. rewrite PTree.gso; eauto. + exploit (P x); simpl. rewrite PTree.gss; eauto. intuition. + apply T.sub_trans with (T.glb hi0 ty); auto. eapply T.glb_left; eauto. + + eapply P; simpl. rewrite PTree.gso; eauto. - inv H. destruct H0 as [P Q]; split; auto; intros. eapply P; simpl. rewrite PTree.gso; eauto. congruence. Qed. @@ -466,12 +466,12 @@ Proof. destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. - destruct (T.sub_dec lo ty); try discriminate. destruct (T.eq hi (T.glb hi ty)); monadInv H. - + subst e'. apply T.sub_trans with hi. - eapply P; eauto. rewrite e0. eapply T.glb_right; eauto. - + apply T.sub_trans with (T.glb hi ty). - eapply (P x). simpl. rewrite PTree.gss; eauto. - eapply T.glb_right; eauto. -- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto. + + subst e'. apply T.sub_trans with hi. + eapply P; eauto. rewrite e0. eapply T.glb_right; eauto. + + apply T.sub_trans with (T.glb hi ty). + eapply (P x). simpl. rewrite PTree.gss; eauto. + eapply T.glb_right; eauto. +- inv H. eapply (P x); simpl. rewrite PTree.gss; eauto. Qed. Lemma type_uses_incr: @@ -502,27 +502,27 @@ Proof. destruct (T.sub_dec lo1 hi2); try discriminate. set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *. destruct (T.eq lo2 lo); destruct (T.eq hi1 hi); monadInv H; simpl in *. - + subst e'; simpl in *. split; auto. + + subst e'; simpl in *. split; auto. + subst e'; simpl in *. split; auto. intros. destruct (peq x r1). - subst x. - rewrite E1 in H. injection H; intros; subst lo0 hi0. - exploit (P r1). rewrite PTree.gss; eauto. intuition. + subst x. + rewrite E1 in H. injection H; intros; subst lo0 hi0. + exploit (P r1). rewrite PTree.gss; eauto. intuition. apply T.sub_trans with (T.glb hi1 hi2); auto. eapply T.glb_left; eauto. eapply P. rewrite PTree.gso; eauto. + subst e'; simpl in *. split; auto. intros. destruct (peq x r2). - subst x. - rewrite E2 in H. injection H; intros; subst lo0 hi0. - exploit (P r2). rewrite PTree.gss; eauto. intuition. + subst x. + rewrite E2 in H. injection H; intros; subst lo0 hi0. + exploit (P r2). rewrite PTree.gss; eauto. intuition. apply T.sub_trans with (T.lub lo1 lo2); auto. eapply T.lub_right; eauto. eapply P. rewrite PTree.gso; eauto. - + split; auto. intros. - destruct (peq x r1). subst x. - rewrite E1 in H. injection H; intros; subst lo0 hi0. - exploit (P r1). rewrite PTree.gso; eauto. rewrite PTree.gss; eauto. intuition. + + split; auto. intros. + destruct (peq x r1). subst x. + rewrite E1 in H. injection H; intros; subst lo0 hi0. + exploit (P r1). rewrite PTree.gso; eauto. rewrite PTree.gss; eauto. intuition. apply T.sub_trans with (T.glb hi1 hi2); auto. eapply T.glb_left; eauto. - destruct (peq x r2). subst x. - rewrite E2 in H. injection H; intros; subst lo0 hi0. - exploit (P r2). rewrite PTree.gss; eauto. intuition. + destruct (peq x r2). subst x. + rewrite E2 in H. injection H; intros; subst lo0 hi0. + exploit (P r2). rewrite PTree.gss; eauto. intuition. apply T.sub_trans with (T.lub lo1 lo2); auto. eapply T.lub_right; eauto. eapply P. rewrite ! PTree.gso; eauto. - inv H; simpl in *. split; intros. @@ -531,7 +531,7 @@ Proof. - inv H; simpl in *. split; intros. eapply P. rewrite PTree.gso; eauto. congruence. apply Q. destruct (T.sub_dec hi2 lo2); auto with coqlib. -- inv H; simpl in *. split; auto. +- inv H; simpl in *. split; auto. Qed. Hint Resolve type_move_incr: ty. @@ -544,24 +544,24 @@ Proof. destruct (peq r1 r2). subst r2. apply T.sub_refl. destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1; destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2. -- destruct (T.sub_dec hi1 lo2). +- destruct (T.sub_dec hi1 lo2). inv H. apply T.sub_trans with hi1. eapply P; eauto. apply T.sub_trans with lo2; auto. eapply P; eauto. destruct (T.sub_dec lo1 hi2); try discriminate. set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *. destruct (T.eq lo2 lo); destruct (T.eq hi1 hi); monadInv H; simpl in *. + subst e'; simpl in *. apply Q; auto. - + subst e'; simpl in *. apply Q; auto. - + subst e'; simpl in *. apply Q; auto. + + subst e'; simpl in *. apply Q; auto. + + subst e'; simpl in *. apply Q; auto. + apply Q; auto. - inv H; simpl in *. destruct (T.sub_dec hi1 lo1). - + apply T.sub_trans with hi1. eapply P; eauto. rewrite PTree.gso; eauto. - apply T.sub_trans with lo1; auto. eapply P. rewrite PTree.gss; eauto. + + apply T.sub_trans with hi1. eapply P; eauto. rewrite PTree.gso; eauto. + apply T.sub_trans with lo1; auto. eapply P. rewrite PTree.gss; eauto. + auto with coqlib. - inv H; simpl in *. destruct (T.sub_dec hi2 lo2). - + apply T.sub_trans with hi2. eapply P. rewrite PTree.gss; eauto. - apply T.sub_trans with lo2; auto. eapply P. rewrite PTree.gso; eauto. + + apply T.sub_trans with hi2. eapply P. rewrite PTree.gss; eauto. + apply T.sub_trans with lo2; auto. eapply P. rewrite PTree.gso; eauto. + auto with coqlib. -- inv H. simpl in Q; auto. +- inv H. simpl in Q; auto. Qed. Lemma solve_rec_incr: @@ -575,12 +575,12 @@ Qed. Lemma solve_rec_sound: forall te r1 r2 q e changed e' changed', - solve_rec e changed q = OK(e', changed') -> In (r1, r2) q -> satisf te e' -> + solve_rec e changed q = OK(e', changed') -> In (r1, r2) q -> satisf te e' -> T.sub (te r1) (te r2). Proof. induction q; simpl; intros. - contradiction. -- destruct a as [r3 r4]; monadInv H. destruct H0. +- destruct a as [r3 r4]; monadInv H. destruct H0. + inv H. eapply type_move_sound; eauto. eapply solve_rec_incr; eauto. + eapply IHq; eauto with ty. Qed. @@ -590,12 +590,12 @@ Lemma type_move_false: type_move e r1 r2 = OK(false, e') -> te_typ e' = te_typ e /\ T.sub (makeassign e r1) (makeassign e r2). Proof. - unfold type_move; intros. + unfold type_move; intros. destruct (peq r1 r2). inv H. split; auto. apply T.sub_refl. unfold makeassign; destruct (te_typ e)!r1 as [[lo1 hi1 s1]|] eqn:E1; destruct (te_typ e)!r2 as [[lo2 hi2 s2]|] eqn:E2. -- destruct (T.sub_dec hi1 lo2). +- destruct (T.sub_dec hi1 lo2). inv H. split; auto. eapply T.sub_trans; eauto. destruct (T.sub_dec lo1 hi2); try discriminate. set (lo := T.lub lo1 lo2) in *. set (hi := T.glb hi1 hi2) in *. @@ -609,17 +609,17 @@ Qed. Lemma solve_rec_false: forall r1 r2 q e changed e', solve_rec e changed q = OK(e', false) -> - changed = false /\ + changed = false /\ (In (r1, r2) q -> T.sub (makeassign e r1) (makeassign e r2)). Proof. induction q; simpl; intros. -- inv H. tauto. +- inv H. tauto. - destruct a as [r3 r4]; monadInv H. exploit IHq; eauto. intros [P Q]. destruct changed; try discriminate. destruct x; try discriminate. exploit type_move_false; eauto. intros [U V]. - split. auto. intros [A|A]. inv A. auto. exploit Q; auto. - unfold makeassign; rewrite U; auto. + split. auto. intros [A|A]. inv A. auto. exploit Q; auto. + unfold makeassign; rewrite U; auto. Qed. Lemma solve_constraints_incr: @@ -638,7 +638,7 @@ Proof. intros e0; functional induction (solve_constraints e0); intros. - inv H. split; intros. unfold makeassign; rewrite H. split; auto with ty. - exploit solve_rec_false. eauto. intros [A B]. eapply B; eauto. + exploit solve_rec_false. eauto. intros [A B]. eapply B; eauto. - eauto. - discriminate. Qed. @@ -646,7 +646,7 @@ Qed. Theorem solve_sound: forall e te, solve e = OK te -> satisf te e. Proof. - unfold solve; intros. monadInv H. + unfold solve; intros. monadInv H. eapply solve_constraints_incr. eauto. eapply solve_constraints_sound; eauto. Qed. @@ -657,17 +657,17 @@ Lemma type_def_complete: satisf te e -> T.sub ty (te x) -> exists e', type_def e x ty = OK e' /\ satisf te e'. Proof. unfold type_def; intros. destruct H as [P Q]. - destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. -- destruct (T.sub_dec ty hi). + destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. +- destruct (T.sub_dec ty hi). destruct (T.eq lo (T.lub lo ty)). exists e; split; auto. split; auto. - econstructor; split; eauto. split; simpl; auto; intros. - rewrite PTree.gsspec in H. destruct (peq x0 x). - inv H. exploit P; eauto. intuition. eapply T.lub_min; eauto. + econstructor; split; eauto. split; simpl; auto; intros. + rewrite PTree.gsspec in H. destruct (peq x0 x). + inv H. exploit P; eauto. intuition. eapply T.lub_min; eauto. eapply P; eauto. elim n. apply T.sub_trans with (te x); auto. eapply P; eauto. - econstructor; split; eauto. split; simpl; auto; intros. - rewrite PTree.gsspec in H. destruct (peq x0 x). + rewrite PTree.gsspec in H. destruct (peq x0 x). inv H. split; auto. apply T.high_bound_majorant; auto. eapply P; eauto. Qed. @@ -689,17 +689,17 @@ Lemma type_use_complete: satisf te e -> T.sub (te x) ty -> exists e', type_use e x ty = OK e' /\ satisf te e'. Proof. unfold type_use; intros. destruct H as [P Q]. - destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. -- destruct (T.sub_dec lo ty). + destruct (te_typ e)!x as [[lo hi s1]|] eqn:E. +- destruct (T.sub_dec lo ty). destruct (T.eq hi (T.glb hi ty)). exists e; split; auto. split; auto. - econstructor; split; eauto. split; simpl; auto; intros. - rewrite PTree.gsspec in H. destruct (peq x0 x). - inv H. exploit P; eauto. intuition. eapply T.glb_max; eauto. + econstructor; split; eauto. split; simpl; auto; intros. + rewrite PTree.gsspec in H. destruct (peq x0 x). + inv H. exploit P; eauto. intuition. eapply T.glb_max; eauto. eapply P; eauto. elim n. apply T.sub_trans with (te x); auto. eapply P; eauto. - econstructor; split; eauto. split; simpl; auto; intros. - rewrite PTree.gsspec in H. destruct (peq x0 x). + rewrite PTree.gsspec in H. destruct (peq x0 x). inv H. split; auto. apply T.low_bound_minorant; auto. eapply P; eauto. Qed. @@ -730,15 +730,15 @@ Proof. - exploit (P r1); eauto. intros [L1 U1]. exploit (P r2); eauto. intros [L2 U2]. destruct (T.sub_dec hi1 lo2). econstructor; econstructor; eauto. - destruct (T.sub_dec lo1 hi2). + destruct (T.sub_dec lo1 hi2). destruct (T.eq lo2 (T.lub lo1 lo2)); destruct (T.eq hi1 (T.glb hi1 hi2)); econstructor; econstructor; split; eauto; split; auto; simpl; intros. - + rewrite PTree.gsspec in H1. destruct (peq x r1). - clear e0. inv H1. split; auto. + + rewrite PTree.gsspec in H1. destruct (peq x r1). + clear e0. inv H1. split; auto. apply T.glb_max. auto. apply T.sub_trans with (te r2); auto. eapply P; eauto. - + rewrite PTree.gsspec in H1. destruct (peq x r2). - clear e0. inv H1. split; auto. + + rewrite PTree.gsspec in H1. destruct (peq x r2). + clear e0. inv H1. split; auto. apply T.lub_min. apply T.sub_trans with (te r1); auto. auto. eapply P; eauto. + rewrite ! PTree.gsspec in H1. destruct (peq x r2). @@ -746,18 +746,18 @@ Proof. destruct (peq x r1). inv H1. split; auto. apply T.glb_max; auto. apply T.sub_trans with (te r2); auto. eapply P; eauto. - + elim n1. apply T.sub_trans with (te r1); auto. - apply T.sub_trans with (te r2); auto. + + elim n1. apply T.sub_trans with (te r1); auto. + apply T.sub_trans with (te r2); auto. - econstructor; econstructor; split; eauto; split. + simpl; intros. rewrite PTree.gsspec in H1. destruct (peq x r2). - inv H1. exploit P; eauto. intuition. + inv H1. exploit P; eauto. intuition. apply T.sub_trans with (te r1); auto. apply T.high_bound_majorant. apply T.sub_trans with (te r1); auto. eapply P; eauto. + destruct (T.sub_dec hi1 lo1); auto. - econstructor; econstructor; split; eauto; split. + simpl; intros. rewrite PTree.gsspec in H1. destruct (peq x r1). - inv H1. exploit P; eauto. intuition. + inv H1. exploit P; eauto. intuition. apply T.low_bound_minorant. apply T.sub_trans with (te r2); auto. apply T.sub_trans with (te r2); auto. eapply P; eauto. @@ -773,7 +773,7 @@ Lemma solve_rec_complete: Proof. induction q; simpl; intros. - econstructor; econstructor; eauto. -- destruct a as [r1 r2]. +- destruct a as [r1 r2]. exploit (type_move_complete te e r1 r2); auto. intros (changed1 & e1 & A & B). exploit (IHq e1 (changed || changed1)); auto. intros (e' & changed' & C & D). exists e'; exists changed'. rewrite A; simpl; rewrite C; auto. @@ -782,26 +782,26 @@ Qed. Lemma solve_constraints_complete: forall te e, satisf te e -> exists e', solve_constraints e = OK e' /\ satisf te e'. Proof. - intros te e. functional induction (solve_constraints e); intros. + intros te e. functional induction (solve_constraints e); intros. - exists e; auto. - exploit (solve_rec_complete te (te_sub e) {| te_typ := te_typ e; te_sub := nil |} false). destruct H; split; auto. simpl; tauto. destruct H; auto. - intros (e1 & changed1 & P & Q). - apply IHr. congruence. + intros (e1 & changed1 & P & Q). + apply IHr. congruence. - exploit (solve_rec_complete te (te_sub e) {| te_typ := te_typ e; te_sub := nil |} false). destruct H; split; auto. simpl; tauto. destruct H; auto. - intros (e1 & changed1 & P & Q). + intros (e1 & changed1 & P & Q). congruence. Qed. Lemma solve_complete: forall te e, satisf te e -> exists te', solve e = OK te'. Proof. - intros. unfold solve. - destruct (solve_constraints_complete te e H) as (e' & P & Q). - econstructor. rewrite P. simpl. eauto. + intros. unfold solve. + destruct (solve_constraints_complete te e H) as (e' & P & Q). + econstructor. rewrite P. simpl. eauto. Qed. End SubSolver. -- cgit