text:
From Test Require Import tactic.

Section FOFProblem.

Variable Universe : Set.
Variable UniverseElement : Universe.

Variable wd_ : Universe -> Universe -> Prop.
Variable col_ : Universe -> Universe -> Universe -> Prop.

Variable col_swap1_1 : (forall A B C : Universe, (col_ A B C -> col_ B A C)).
Variable col_swap2_2 : (forall A B C : Universe, (col_ A B C -> col_ B C A)).
Variable col_triv_3 : (forall A B : Universe, col_ A B B).
Variable wd_swap_4 : (forall A B : Universe, (wd_ A B -> wd_ B A)).
Variable col_trans_5 : (forall P Q A B C : Universe, ((wd_ P Q /\ (col_ P Q A /\ (col_ P Q B /\ col_ P Q C))) -> col_ A B C)).

Theorem pipo_6 : (forall O E Eprime P A B C D A1 B1 C1 D1 C1prime M D1prime N : Universe, ((wd_ O E /\ (wd_ P B /\ (wd_ A B /\ (wd_ O M /\ (wd_ M C1 /\ (wd_ C A /\ (wd_ P A /\ (wd_ C1 C1prime /\ (wd_ O C1prime /\ (wd_ A1 O /\ (wd_ O C1 /\ (wd_ E Eprime /\ (wd_ O Eprime /\ (wd_ P C /\ (wd_ C1prime A1 /\ (wd_ O B1 /\ (wd_ M C1prime /\ (wd_ N O /\ (wd_ D1 N /\ (wd_ D1 D1prime /\ (wd_ N D1prime /\ (wd_ D1prime O /\ (wd_ O D1 /\ (wd_ P D /\ (wd_ A1 Eprime /\ (wd_ D1prime B1 /\ (wd_ D B /\ (col_ P A B /\ (col_ P C D /\ (col_ O E A1 /\ (col_ O E B1 /\ (col_ O E C1 /\ (col_ O E D1 /\ (col_ O M N /\ (col_ O A1 C1prime /\ (col_ N D1 D1prime /\ (col_ M C1 C1prime /\ (col_ O C1prime D1prime /\ (col_ O A1 C1 /\ col_ O C1 D1))))))))))))))))))))))))))))))))))))))) -> col_ O C1 C1prime)).
Proof.
  time tac.
Qed.

End FOFProblem.

author: janicicpredrag

repo: Larus

save_path: github-repos/coq/janicicpredrag-Larus


Require Import Coq.Classes.Morphisms.
Require Import Coq.Relations.Relation_Definitions.
Require Import Crypto.Util.Decidable.
Require Import Crypto.Util.GlobalSettings.

Definition sumwise {A B} (RA:relation A) (RB : relation B) : relation (A + B)
  := fun x y => match x, y with
                | inl x', inl y' => RA x' y'
                | inr x', inr y' => RB x' y'
                | _, _ => False
                end.

Global Instance Equivalence_sumwise
  : forall {A B} {RA:relation A} {RB:relation B}
           {RA_equiv:Equivalence RA} {RB_equiv:Equivalence RB},
    Equivalence (sumwise RA RB).
Proof.
  intros A B RA RB RA_equiv RB_equiv.
  split; repeat intros [?|?]; simpl; trivial; destruct RA_equiv, RB_equiv; try tauto; eauto.
Qed.

Arguments sumwise {A B} _ _ _ _.

Ltac congruence_sum_step :=
  match goal with
  | [ H : inl _ = inr _ |- _ ] => solve [ inversion H ]
  | [ H : inr _ = inl _ |- _ ] => solve [ inversion H ]
  | [ H : inl _ = inl _ |- _ ] => inversion H; clear H
  | [ H : inr _ = inr _ |- _ ] => inversion H; clear H
  end.
Ltac congruence_sum := repeat congruence_sum_step.

Local Hint Extern 0 => solve [ solve_decidable_transparent ] : typeclass_instances.
Global Instance dec_sumwise {A B RA RB} {HA : DecidableRel RA} {HB : DecidableRel RB} : DecidableRel (@sumwise A B RA RB) | 10.
Proof.
  intros [x|x] [y|y]; exact _.
Qed.

(** ** Equality for [sum] *)
Section sum.
  Local Notation sum_code u v
    := (match u, v with
        | inl u', inl v'
        | inr u', inr v'
          => u' = v'
        | inl _, _
        | inr _, _
          => False
        end).

  (** *** Equality of [sum] is a [match] *)
  Definition path_sum {A B} (u v : sum A B) (p : sum_code u v)
    : u = v.
  Proof. destruct u, v; first [ apply f_equal | exfalso ]; exact p. Defined.

  (** *** Equivalence of equality of [sum] with [sum_code] *)
  Definition unpath_sum {A B} {u v : sum A B} (p : u = v)
    : sum_code u v.
  Proof. subst v; destruct u; reflexivity. Defined.

  Definition path_sum_iff {A B}
             (u v : @sum A B)
    : u = v <-> sum_code u v.
  Proof.
    split; [ apply unpath_sum | apply path_sum ].
  Defined.

  (** *** Eta-expansion of [@eq (sum _ _)] *)
  Definition path_sum_eta {A B} {u v : @sum A B} (p : u = v)
    : p = path_sum u v (unpath_sum p).
  Proof. destruct u, p; reflexivity. Defined.

  (** *** Induction principle for [@eq (sum _ _)] *)
  Definition path_sum_rect {A B} {u v : @sum A B} (P : u = v -> Type)
             (f : forall p, P (path_sum u v p))
    : forall p, P p.
  Proof. intro p; specialize (f (unpath_sum p)); destruct u, p; exact f. Defined.
  Definition path_sum_rec {A B u v} (P : u = v :> @sum A B -> Set) := path_sum_rect P.
  Definition path_sum_ind {A B u v} (P : u = v :> @sum A B -> Prop) := path_sum_rec P.
End sum.

(** ** Useful Tactics *)
(** *** [inversion_sum] *)
Ltac induction_path_sum H :=
  induction H as [H] using path_sum_rect;
  try match type of H with
      | False => exfalso; exact H
      end.
Ltac inversion_sum_step :=
  match goal with
  | [ H : inl _ = inl _ |- _ ]
    => induction_path_sum H
  | [ H : inl _ = inr _ |- _ ]
    => induction_path_sum H
  | [ H : inr _ = inl _ |- _ ]
    => induction_path_sum H
  | [ H : inr _ = inr _ |- _ ]
    => induction_path_sum H
  end.
Ltac inversion_sum := repeat inversion_sum_step.


text:
(* Disable notation conflict warnings *)
Set Warnings "-notation-overridden".

From mathcomp.ssreflect
Require Import ssreflect ssrnat prime ssrbool.

Require Import Name.
Require Import Id.
Require Import Core.
Require Import CoreFVs.
Require Import CoreUtils.

Require Import Coq.Lists.List.
Require Import Coq.Bool.Bool.
Import ListNotations.

Require Import Proofs.GHC.Base.

Require Import Proofs.Axioms.

Require Import Proofs.Base.
Require Import Proofs.GhcTactics.
Require Import Proofs.Forall.
Require Import Proofs.Unique.
Require Import Proofs.CoreFVs.
Require Import Proofs.VarSet.
Require Import Proofs.VarEnv.
Require Import Proofs.CoreInduct.
Require Import Proofs.Var.

Import GHC.Base.Notations.

Set Bullet Behavior "Strict Subproofs".

Lemma contrapositive : forall (A B:Prop), (A -> B) -> (~ B) -> (~ A).
Proof.
  intros.
  intro h. apply H in h. apply H0. auto.
Qed.

Lemma and_iff_compat_both:
  forall A B C D : Prop,
    A <-> C -> B <-> D ->
    A /\ B <-> C /\ D.
Proof. intros. intuition. Qed.

Lemma Forall_iff:
  forall a P Q (xs : list a),
    Forall (fun x => P x <-> Q x) xs ->
    Forall P xs <-> Forall Q xs.
Proof. intros. rewrite -> !Forall_forall in *. firstorder. Qed.

(** * Core invariants related to variables and scope *)

(** ** The invariants *)

(**
First we define invariants for [Var] that are independent of scope, namely:
- It is a localVar iff the unique is local.
- The [Unique] cached in the [Var] is the same as the [Unique] of the name
  of the var.
- The var must be an identifier (i.e. a term variable)
- but not one that is a coercion variable.
*)
Definition GoodVar (v : Var) : Prop :=
  isLocalVar v = isLocalUnique (varUnique v) /\
  varUnique v = nameUnique (varName v) /\
  isId v = true /\
  isCoVar v = false.

Definition GoodLocalVar (v : Var) : Prop :=
  GoodVar v /\ isLocalVar v = true.

(**

Next we define when a variable occurrence is ok in a given scope.
 * Global variables are always ok (not yet tracked).
 * Local variables are ok if they are in scope, and
   are almost the same as the binder; i.e., only the
   [idInfo] may vary

*)

Definition WellScopedVar (v : Var) (in_scope : VarSet) : Prop :=
  if isLocalVar v then
   match lookupVarSet in_scope v with
    | None => False
    | Some v' => almostEqual v v' /\ GoodVar v
    end
  else GoodVar v (* we do not track global variables yet *).

(**

Finally, we lift this to whole expressions, keeping track of the variables
that are in [in_scope]. Remember that GHC allows shadowing!

*)

Definition WellScopedTickish (x : Tickish Var)(in_scope : VarSet) : Prop :=
  match x with
  | Breakpoint _ ids => Forall (fun e => WellScopedVar e in_scope) ids
  | _ => True
  end.

Fixpoint WellScoped (e : CoreExpr) (in_scope : VarSet) {struct e} : Prop :=
  match e with
  | Mk_Var v => WellScopedVar v in_scope
  | Lit l => True
  | App e1 e2 => WellScoped e1 in_scope /\  WellScoped e2 in_scope
  | Lam v e => GoodLocalVar v /\ WellScoped e (extendVarSet in_scope v)
  | Let bind body =>
      WellScopedBind bind in_scope /\
      WellScoped body (extendVarSetList in_scope (bindersOf bind))
  | Case scrut bndr ty alts  =>
    WellScoped scrut in_scope /\
    GoodLocalVar bndr /\
    Forall' (fun alt =>
      Forall GoodLocalVar (snd (fst alt)) /\
      let in_scope' := extendVarSetList in_scope (bndr :: snd (fst alt)) in
      WellScoped (snd alt) in_scope') alts
  | Cast e _ =>   WellScoped e in_scope
  | Tick t e =>   WellScoped e in_scope /\ WellScopedTickish t in_scope
  | Type_ _  =>   True
  | Coercion _ => True
  end
with WellScopedBind (bind : CoreBind) (in_scope : VarSet) : Prop :=
  match bind with
  | NonRec v rhs =>
    GoodLocalVar v /\
    WellScoped rhs in_scope
  | Rec pairs =>
    Forall (fun p => GoodLocalVar (fst p)) pairs /\
    NoDup (map varUnique (map fst pairs)) /\
    Forall' (fun p => WellScoped (snd p) (extendVarSetList in_scope (map fst pairs))) pairs
  end.

Definition WellScopedAlt bndr (alt : CoreAlt) in_scope  :=
    Forall GoodLocalVar (snd (fst alt)) /\
    let in_scope' := extendVarSetList in_scope (bndr :: snd (fst alt)) in
    WellScoped (snd alt) in_scope'.

(**

A [CoreProgram] can be treated like one big recursive group, despite that it
is a sequence of [Rec] and [NonRec] bindings.

*)
Definition WellScopedProgram (pgm : CoreProgram) : Prop :=
   NoDup (map varUnique (bindersOfBinds pgm)) /\
   Forall' (fun p => WellScoped (snd p) (mkVarSet (bindersOfBinds pgm))) (flattenBinds pgm).

(** ** Lemmas *)

(** *** Lemmas about [GoodLocalVar] *)

Lemma GoodLocalVar_uniqAway:
  forall vss v, GoodLocalVar v -> GoodLocalVar (uniqAway vss v).
Proof.
  intros.
  unfold GoodLocalVar, GoodVar in *.
  destruct H; destruct H; destruct H1. destruct H2.
  rewrite isLocalVar_uniqAway.
  rewrite isLocalUnique_uniqAway.
  rewrite isId_uniqAway.
  rewrite isCoVar_uniqAway.
  repeat split; auto.
  rewrite nameUnique_varName_uniqAway; auto.
Qed.

Lemma GoodLocalVar_asJoinId_mkSysLocal:
  forall s u ty n,
  isLocalUnique u = true ->
  GoodLocalVar (asJoinId (mkSysLocal s u ty) n).
Proof.
  intros.
  split; only 1: split.
  * destruct u. symmetry. apply H.
  * split. destruct u. reflexivity.
    auto.
  * destruct u. reflexivity.
Qed.

Lemma GoodLocalVar_almostEqual:
  forall v1 v2,
  GoodLocalVar v1 ->
  almostEqual v1 v2 ->
  GoodLocalVar v2.
Proof.
  intros.
  destruct H. destruct H.
  induction H0.
  * split; only 1: split; assumption.
  * split; only 1: split; assumption.
  * split; only 1: split; assumption.
Qed.

Lemma GoodVar_almostEqual :
  forall v1 v2,
    GoodVar v1 -> almostEqual v1 v2 -> GoodVar v2.
Proof.
  move => v1 v2.
  elim => h1 [h2 [h3 h4]].
  move => h. inversion h.
  all: unfold GoodVar.
  all: repeat split.
  all: rewrite <- H in *.
  all: simpl in *.
  all: try done.
Qed.

(** *** Structural lemmas *)

Lemma WellScopedVar_extendVarSet:
  forall v vs,
  GoodVar v ->
  WellScopedVar v (extendVarSet vs v).
Proof.
  intros.
  unfold WellScopedVar.
  rewrite lookupVarSet_extendVarSet_self.
  destruct_match.
  * split. apply almostEqual_refl. trivial.
  * trivial.
Qed.

Lemma WellScoped_varToCoreExpr:
  forall v isvs,
  WellScopedVar v isvs -> WellScoped (varToCoreExpr v) isvs.
Proof.
  intros.
  destruct v; simpl; try trivial.
  unfold varToCoreExpr; simpl.
  destruct_match; simpl; try trivial.
Qed.

Lemma WellScoped_Lam:
  forall v e isvs,
  WellScoped (Lam v e) isvs <-> GoodLocalVar v /\ WellScoped e (extendVarSet isvs v).
Proof. intros. reflexivity. Qed.

Lemma WellScoped_mkLams:
  forall vs e isvs,
  WellScoped (mkLams vs e) isvs <-> Forall GoodLocalVar vs /\ WellScoped e (extendVarSetList isvs vs).
Proof.
  induction vs; intros.
  * intuition.
  * simpl.
    rewrite extendVarSetList_cons.
    rewrite Forall_cons_iff.
    rewrite and_assoc.
    rewrite <- (IHvs _ _).
    reflexivity.
Qed.

Lemma WellScoped_mkVarApps:
  forall e vs isvs,
  WellScoped e isvs ->
  Forall (fun v => WellScopedVar v isvs) vs ->
  WellScoped (mkVarApps e vs) isvs.
Proof.
  intros.
  unfold mkVarApps.
  rewrite Foldable.hs_coq_foldl_list.
  revert e H.
  induction H0; intros.
  * simpl. intuition.
  * simpl.
    apply IHForall; clear IHForall.
    simpl.
    split; try assumption.
    apply WellScoped_varToCoreExpr; assumption.
Qed.

Lemma WellScoped_MkLetRec: forall pairs body isvs,
  WellScoped (mkLetRec pairs body) isvs <-> WellScoped (Let (Rec pairs) body) isvs .
Proof.
  intros.
  unfold mkLetRec.
  destruct pairs; try reflexivity.
  simpl.
  rewrite extendVarSetList_nil.
  split; intro; repeat split; try constructor; intuition.
Qed.

Lemma WellScoped_MkLet: forall bind body isvs,
  WellScoped (mkLet bind body) isvs <-> WellScoped (Let bind body) isvs .
Proof.
  intros.
  unfold mkLet.
  destruct bind; try reflexivity.
  destruct l; try reflexivity.
  simpl.
  rewrite extendVarSetList_nil.
  split; intro; repeat split; try constructor; intuition.
Qed.

(** *** Lemmas related to [StrongSubset] *)

Lemma WellScopedVar_StrongSubset : forall e vs1 vs2,
    WellScopedVar e vs1 -> StrongSubset vs1 vs2 -> WellScopedVar e vs2.
Proof.
  intros v vs1 vs2 WS SS.
  unfold WellScopedVar, StrongSubset in *.
  destruct_match; only 2: trivial.
  specialize (SS v).
  destruct (lookupVarSet vs1 v); try contradiction.
  destruct (lookupVarSet vs2 v) eqn:LV2; try contradiction.
  intuition.
  eapply almostEqual_trans with (v2 := v0); auto.
Qed.

Lemma WellScopedTickish_StrongSubset : forall e vs1 vs2,
    WellScopedTickish e vs1 -> StrongSubset vs1 vs2 -> WellScopedTickish e vs2.
Proof.
  move => e vs1 vs2 WS SS.
  unfold WellScopedTickish, StrongSubset in *.
  destruct_match; try done.
  eapply Forall_impl; eauto.
  move=> a h. eapply WellScopedVar_StrongSubset; eauto. simpl in h.
  auto.
Qed.

Lemma WellScoped_StrongSubset : forall e vs1 vs2,
    WellScoped e vs1 -> StrongSubset vs1 vs2 -> WellScoped e vs2.
Proof.
  intro e.
  apply (core_induct e); intros; try (destruct binds);
    unfold WellScoped in *; fold WellScoped in *; eauto.
  - eapply WellScopedVar_StrongSubset; eauto.
  - destruct H1. split; eauto.
  - split; only 1: apply H0.
    destruct H0 as [_ H0].
    eapply H; eauto.
    unfold StrongSubset in *.
    intro var.
    specialize (H1 var).
    unfold CoreBndr in v. (* make sure that the type class looks right.*)
    destruct (v GHC.Base.== var) eqn:Eq.
    + rewrite lookupVarSet_extendVarSet_eq; auto.
      rewrite lookupVarSet_extendVarSet_eq; auto.
      eapply almostEqual_refl.
    + rewrite lookupVarSet_extendVarSet_neq.
      destruct (lookupVarSet vs1 var) eqn:IN; auto.
      rewrite lookupVarSet_extendVarSet_neq.
      auto.
      intro h;
      rewrite Eq in h; discriminate.
      intro h;
      rewrite Eq in h; discriminate.
  - destruct H1 as [[GLV WE] Wb].
     split; only 1: split; eauto.
     eapply H0; eauto.
     eapply StrongSubset_extendVarSetList.
     auto.
  - destruct H1 as [[WE1 [WE2 WE3]] Wb].
     repeat split; auto.
     rewrite -> Forall'_Forall in *.
     rewrite -> Forall_forall in *.
     intros h IN. destruct h as [v rhs].
     specialize (WE3 (v,rhs)).
     simpl in *.
     eauto using StrongSubset_extendVarSetList.
     eauto using StrongSubset_extendVarSetList.
  - destruct H1 as [W1 [W2 W3]].    split; only 2: split; eauto.
     rewrite -> Forall'_Forall in *.
     rewrite -> Forall_forall in *.
     intros h IN. destruct h as [[dc pats] rhs].
     specialize (H0 dc pats rhs IN).
     specialize (W3 (dc,pats,rhs) IN).
     simpl in *.
     destruct W3 as [GLV WS].
     eauto using StrongSubset_extendVarSetList.
  - move: H0 => [? ?].
    eauto using WellScopedTickish_StrongSubset.
Qed.

(** *** Relation to [exprFreeVars] *)

Require Import Proofs.VarSetFSet.

Lemma WellScoped_subset:
  forall e vs,
    WellScoped e vs -> subVarSet (exprFreeVars e) vs = true.
Proof.
  intro e.
  apply (core_induct e); intros.
  - unfold WellScoped, WellScopedVar in *.
    destruct (isLocalVar v) eqn:HisLocal.
    + destruct (lookupVarSet vs v) eqn:Hl; try contradiction.
      rewrite -> exprFreeVars_Var by assumption.
      rewrite subVarSet_unitVarSet.
      eapply lookupVarSet_elemVarSet; eassumption.
    + rewrite -> exprFreeVars_global_Var by assumption.
      apply subVarSet_emptyVarSet.
  - apply subVarSet_emptyVarSet.
  - simpl in H1.
    rewrite exprFreeVars_App.
    rewrite subVarSet_unionVarSet.
    rewrite andb_true_iff.
    intuition.
  - simpl in H0.
    destruct H0.
    rewrite exprFreeVars_Lam.
    apply H in H1.
    set_b_iff. fsetdec.
  - destruct binds as [v rhs | pairs].
    + simpl in H1. decompose [and] H1; clear H1.
      rewrite exprFreeVars_Let_NonRec.
      apply H in H5.
      apply H0 in H3.
      rewrite -> extendVarSetList_cons, extendVarSetList_nil in H3.
      set_b_iff. fsetdec.
    + simpl in H1. decompose [and] H1; clear H1.
      rewrite -> Forall'_Forall in H6.
      rewrite exprFreeVars_Let_Rec.
      apply H0 in H3; clear H0.
      rewrite Core.bindersOf_Rec_cleanup in H3.
      apply subVarSet_delVarSetList_extendVarSetList_dual.
      unfold is_true.
      rewrite -> subVarSet_unionVarSet, andb_true_iff; split.
      * apply subVarSet_exprsFreeVars.
        rewrite -> Forall_map, Forall_forall in *.
        intros [v rhs] HIn. simpl in *.
        apply (H _ _ HIn).
        apply (H6 _ HIn).
      * assumption.
  - simpl in H1. decompose [and] H1; clear H1.
    rewrite -> Forall'_Forall in H5.
    rewrite exprFreeVars_Case.
    rewrite -> subVarSet_unionVarSet, andb_true_iff; split.
    * apply H; assumption.
    * apply subVarSet_mapUnionVarSet.
      rewrite -> Forall_forall in *.
      intros [[dc pats] rhs] HIn.
      specialize (H5 _ HIn). destruct H5. simpl in *.
      (* Some reordering is needed here. This is a bit smelly,
         maybe there should be a [rev] in [exprFreeVars_Case] already? *)
      rewrite <- delVarSetList_rev.
      rewrite rev_app_distr.
      rewrite delVarSetList_app.
      rewrite !delVarSetList_rev.
      rewrite <- delVarSetList_app.
      simpl.
      apply subVarSet_delVarSetList_extendVarSetList_dual.
      apply (H0 _ _ _ HIn).
      assumption.
  - rewrite exprFreeVars_Cast. apply H; assumption.
  - rewrite exprFreeVars_Tick.
    simpl in H0. move: H0 => [a b].
    destruct tickish; unfold tickishFreeVars in *; hs_simpl;
      try (apply H; assumption).
    simpl in b.
    rewrite -> subVarSet_unionVarSet, andb_true_iff; split.
    eauto.
    set_b_iff.
    move=> x InX.
    rewrite -> filter_iff in InX; try apply RespectsVar_isLocalVar.
    move: InX => [i0 i1].
    rewrite -> Forall_forall in b.
    rewrite -> extendVarSetList_iff in i0.
    destruct i0; try done.
    unfold In.
    move: (elem_exists_in _ _ H0) => [y [Iny eqy]].
    move: (b _ Iny) => WSy.
    unfold WellScopedVar in WSy.

    rewrite (RespectsVar_isLocalVar eqy) in i1.
    rewrite i1 in WSy.
    elim h: (lookupVarSet vs y) => [z|].
    erewrite (elemVarSet_eq _ eqy); eauto.
    eapply lookupVarSet_elemVarSet; eauto.
    rewrite h in WSy. done.
  - apply subVarSet_emptyVarSet.
  - apply subVarSet_emptyVarSet.
Qed.

(** *** Freshness *)

Lemma WellScopedVar_extendVarSetList_l:
  forall v vs1 vs2,
  WellScopedVar v vs1 ->
  elemVarSet v (mkVarSet vs2) = false ->
  WellScopedVar v (extendVarSetList vs1 vs2).
Proof.
  intros.
  unfold WellScopedVar in *.
  destruct_match; only 2: assumption.
  destruct_match; only 2: contradiction.
  rewrite lookupVarSet_extendVarSetList_l.
  rewrite Heq0.
  assumption.
  rewrite H0.
  auto.
Qed.

Lemma WellScopedVar_extendVarSetList_r:
  forall v vs1 vs2,
  Forall GoodVar vs2 ->
  List.In v vs2 ->
  NoDup (map varUnique vs2) ->
  WellScopedVar v (extendVarSetList vs1 vs2).
Proof.
  intros.
  unfold WellScopedVar in *.
  assert (Gv: GoodVar v).
   { rewrite -> Forall_forall in *. auto. }
  destruct_match.
  rewrite -> lookupVarSet_extendVarSetList_self_in by assumption.
  intuition.
  apply almostEqual_refl.
  assumption.
Qed.

Lemma WellScopedVar_extendVarSetList_fresh_under v vs vs1 vs2 :
  disjointVarSet (delVarSetList (exprFreeVars (Mk_Var v)) (rev vs2))
                 (mkVarSet vs1) = true ->
  WellScopedVar v (extendVarSetList (extendVarSetList vs vs1) vs2) <->
  WellScopedVar v (extendVarSetList vs vs2).
Proof.
    intro H.
    unfold WellScopedVar.
    destruct_match; only 2: reflexivity.
    enough (lookupVarSet (extendVarSetList (extendVarSetList vs vs1) vs2) v =
            lookupVarSet (extendVarSetList vs vs2) v) as Htmp
      by (rewrite Htmp; reflexivity).
    rewrite -> exprFreeVars_Var in H by assumption.
    rewrite delVarSetList_rev in H.
    clear -H.
    (* duplication with isJoinPointsValid_fresh_updJPSs_aux here *)
    induction vs2 using rev_ind.
    + rewrite !extendVarSetList_nil.
      rewrite delVarSetList_nil in H.
      revert vs; induction vs1; intros.
      - rewrite extendVarSetList_nil.
        reflexivity.
      - rewrite extendVarSetList_cons.
        rewrite -> fold_is_true in H.
        rewrite -> disjointVarSet_mkVarSet_cons in H.
        destruct H.
        rewrite -> IHvs1 by assumption.
        apply lookupVarSet_extendVarSet_neq.
        contradict H.
        rewrite not_false_iff_true.
        apply H.
    + rewrite -> delVarSetList_app, delVarSetList_cons, delVarSetList_nil in H.
      rewrite -> !extendVarSetList_append, !extendVarSetList_cons, !extendVarSetList_nil.
      destruct (x GHC.Base.== v) eqn:?.
      -- rewrite -> !lookupVarSet_extendVarSet_eq by assumption.
         reflexivity.
      -- rewrite <- not_true_iff_false in Heqb.
         rewrite -> !lookupVarSet_extendVarSet_neq by assumption.
         apply IHvs2.
         rewrite -> fold_is_true in *.
         rewrite -> disjointVarSet_mkVarSet in *.
         eapply Forall_impl; only 2: eapply H. intros v2 ?.
         cbv beta in H0.
         rewrite -> delVarSet_elemVarSet_false in H0; only 1: assumption.
         clear -Heqb.
         apply elemVarSet_delVarSetList_false_l.
         unfold is_true in Heqb.
         rewrite -> not_true_iff_false in Heqb.
         apply Heqb.
Qed.

(* There are a number of variants of the freshness lemmas.
   The simplest one that implies all others is this, so lets
   only do one induction:
*)

Lemma WellScoped_extendVarSetList_fresh_under:
  forall vs1 vs2 e vs,
  disjointVarSet (delVarSetList (exprFreeVars e) vs2) (mkVarSet vs1)  = true ->
  WellScoped e (extendVarSetList (extendVarSetList vs vs1) vs2) <->
  WellScoped e (extendVarSetList vs vs2).
Proof.
 (* This proof is similar to isJoinPointsValid_fresh_updJPSs_aux
    In particular, proving the assumtion [disjointVarSet ..] for all the inductive
    cases is identical (although here we have more inductive cases than there.
    Once could common it up with a deidcated induction rule. Or live with the duplication.
  *)
  intros.
  rewrite <- delVarSetList_rev in H.
  revert vs2 vs H.
  apply (core_induct e); intros.
  * simpl.
    eapply WellScopedVar_extendVarSetList_fresh_under; eauto.
  * reflexivity.
  * simpl.
    apply and_iff_compat_both.
    - apply H.
      eapply disjointVarSet_subVarSet_l; only 1: apply H1.
      apply subVarSet_delVarSetList_both.
      rewrite exprFreeVars_App.
      set_b_iff; fsetdec.
    - apply H0.
      eapply disjointVarSet_subVarSet_l; only 1: apply H1.
      apply subVarSet_delVarSetList_both.
      rewrite exprFreeVars_App.
      set_b_iff; fsetdec.
  * simpl.
    apply and_iff_compat_both; try reflexivity.
    rewrite <- !extendVarSetList_singleton.
    rewrite <- !extendVarSetList_append with (vs1 := vs2).
    apply H.
    rewrite -> exprFreeVars_Lam in H0.
    rewrite rev_app_distr.
    simpl.
    rewrite delVarSetList_cons.
    assumption.
  * simpl.
    apply and_iff_compat_both.
    - destruct binds as [v rhs | pairs].
      + simpl.
        apply and_iff_compat_both; only 1: reflexivity.
        apply H.
        eapply disjointVarSet_subVarSet_l; only 1: apply H1.
        apply subVarSet_delVarSetList_both.
        rewrite exprFreeVars_Let_NonRec.
        set_b_iff; fsetdec.
      + simpl.
        repeat apply and_iff_compat_both; try reflexivity.
        rewrite !Forall'_Forall.
        apply Forall_iff.
        rewrite Forall_forall.
        intros [v rhs] HIn.
        rewrite <- !extendVarSetList_append with (vs1 := vs2).
        apply (H _ _ HIn).
        eapply disjointVarSet_subVarSet_l; only 1: apply H1.
        rewrite rev_app_distr; simpl.
        rewrite delVarSetList_app.
        apply subVarSet_delVarSetList_both.
        rewrite exprFreeVars_Let_Rec.
        pose proof (subVarSet_exprFreeVars_exprsFreeVars _ _ _ HIn).
        rewrite delVarSetList_rev.
        apply subVarSet_delVarSetList_both.
        set_b_iff; fsetdec.
    - rewrite <- !extendVarSetList_append with (vs1 := vs2).
      apply H0.
      eapply disjointVarSet_subVarSet_l; only 1: apply H1; clear H1.
      rewrite -> rev_app_distr, delVarSetList_app.
      apply subVarSet_delVarSetList_both.
      destruct binds as [v rhs | pairs].
      -- rewrite exprFreeVars_Let_NonRec.
         simpl.
         rewrite -> delVarSetList_cons, delVarSetList_nil.
         set_b_iff; fsetdec.
      -- rewrite exprFreeVars_Let_Rec.
         simpl. rewrite Core.bindersOf_Rec_cleanup.
         rewrite delVarSetList_rev.
         apply subVarSet_delVarSetList_both.
         set_b_iff; fsetdec.

  * simpl.
    repeat apply and_iff_compat_both; try reflexivity.
    - apply H.
      eapply disjointVarSet_subVarSet_l; only 1: apply H1; clear H1.
      apply subVarSet_delVarSetList_both.
      rewrite exprFreeVars_Case.
      set_b_iff; fsetdec.
    - rewrite !Forall'_Forall.
      apply Forall_iff.
      rewrite Forall_forall.
      intros [[dc pats] rhs] HIn; simpl.
      repeat apply and_iff_compat_both; try reflexivity.
      rewrite <- !extendVarSetList_append with (vs1 := vs2).
      apply (H0 _ _ _ HIn).
      eapply disjointVarSet_subVarSet_l; only 1: apply H1.
      rewrite rev_app_distr; simpl.
      rewrite -> !delVarSetList_app, delVarSetList_cons, delVarSetList_nil.
      apply subVarSet_delVarSetList_both.
      rewrite exprFreeVars_Case.
      unfold is_true.
      match goal with HIn : List.In _ ?xs |- context [mapUnionVarSet ?f ?xs] =>
        let H := fresh in
        epose proof (mapUnionVarSet_In_subVarSet f HIn) as H ; simpl in H end.
      rewrite -> delVarSetList_rev, <- delVarSetList_single, <- delVarSetList_app.
      set_b_iff; fsetdec.
  * apply H.
    eapply disjointVarSet_subVarSet_l; only 1: apply H0.
    apply subVarSet_delVarSetList_both.
    rewrite exprFreeVars_Cast.
    set_b_iff; fsetdec.
  * simpl.
    eapply and_iff_compat_both.
    ++ apply H.
       eapply disjointVarSet_subVarSet_l; only 1: apply H0.
       apply subVarSet_delVarSetList_both.
       rewrite exprFreeVars_Tick.
       set_b_iff; fsetdec.
    ++ destruct tickish; try done.
       simpl.
       rewrite -> exprFreeVars_Tick in H0.
       apply Forall_iff.
       rewrite Forall_forall.
       move=> x In.
       eapply WellScopedVar_extendVarSetList_fresh_under.
       unfold tickishFreeVars in H0.
       eapply disjointVarSet_subVarSet_l.
       eapply H0.
       eapply subVarSet_delVarSetList_both.
       elim LV: (isLocalVar x).
       -- rewrite (exprFreeVars_Var x LV).
          rewrite subVarSet_unitVarSet.
          hs_simpl. apply /orP. right.
          rewrite elemVarSet_filterVarSet => //.
          apply /andP. split. auto.
          hs_simpl.
          apply list_in_elem.
          auto.
       -- rewrite (exprFreeVars_global_Var x LV).
          apply subVarSet_emptyVarSet.
  * reflexivity.
  * reflexivity.
Qed.

Lemma WellScoped_extendVarSetList_fresh:
  forall vs e vs1,
  disjointVarSet (exprFreeVars e) (mkVarSet vs) = true ->
  WellScoped e (extendVarSetList vs1 vs) <->
  WellScoped e vs1.
Proof.
  intros.
  epose proof (WellScoped_extendVarSetList_fresh_under vs [] e vs1 _).
  rewrite !extendVarSetList_nil in H0.
  eassumption.
  Unshelve.
  rewrite delVarSetList_nil. assumption.
Qed.

Lemma WellScoped_extendVarSet_fresh:
  forall v e vs,
  elemVarSet v (exprFreeVars e) = false ->
  WellScoped e (extendVarSet vs v) <-> WellScoped e vs.
Proof.
  intros.
  epose proof (WellScoped_extendVarSetList_fresh [v] e vs _).
  rewrite -> extendVarSetList_cons,extendVarSetList_nil in H0.
  assumption.
  Unshelve.
  rewrite -> fold_is_true in *.
  rewrite -> disjointVarSet_mkVarSet_cons, disjointVarSet_mkVarSet_nil.
  intuition congruence.
Qed.

Lemma WellScoped_extendVarSetList_fresh_between:
  forall (vs1 vs2 vs3 : list Var) (e : CoreExpr) (vs : VarSet),
  disjointVarSet (delVarSetList (exprFreeVars e) vs3) (mkVarSet vs2) = true ->
  WellScoped e (extendVarSetList vs ((vs1 ++ vs2) ++ vs3)) <->
  WellScoped e (extendVarSetList vs (vs1 ++ vs3)).
Proof.
  intros.
  rewrite <- app_assoc.
  rewrite !extendVarSetList_append.
  apply WellScoped_extendVarSetList_fresh_under.
  assumption.
Qed.

(** *** The invariants respect [StrongSubset] *)

Instance Respects_StrongSubset_WellScopedVar v : Respects_StrongSubset (WellScopedVar v).
Proof.
  intros ????.
  unfold WellScopedVar in *.
  destruct_match; only 2: assumption.
  destruct_match; only 2: contradiction.
  specialize (H v).
  rewrite Heq0 in H.
  destruct_match; only 2: contradiction.
  intuition.
  eapply almostEqual_trans; eassumption.
Qed.

Instance Respects_StrongSubset_WellScopedTickish v : Respects_StrongSubset (WellScopedTickish v).
Proof.
  intros ????.
  unfold WellScopedTickish in *.
  destruct v; try done.
  rewrite -> Forall_forall in *.
  move=> x In.
  move: (H0 x In) => h.
  eapply Respects_StrongSubset_WellScopedVar; eauto.
Qed.

Instance Respects_StrongSubset_WellScoped e : Respects_StrongSubset (WellScoped e).
Proof.
  apply (core_induct e); intros; simpl.
  * apply Respects_StrongSubset_WellScopedVar.
  * apply Respects_StrongSubset_const.
  * apply Respects_StrongSubset_and; assumption.
  * apply Respects_StrongSubset_and; try apply Respects_StrongSubset_const.
    apply Respects_StrongSubset_extendVarSet.
    assumption.
  * apply Respects_StrongSubset_and.
    - destruct_match.
      + apply Respects_StrongSubset_and; try apply Respects_StrongSubset_const.
        assumption.
      + simpl.
        repeat apply Respects_StrongSubset_and; try apply Respects_StrongSubset_const.
        setoid_rewrite Forall'_Forall.
        apply Respects_StrongSubset_forall.
        rewrite Forall_forall.
        intros [v rhs] HIn.
        specialize (H _ _ HIn).
        apply Respects_StrongSubset_extendVarSetList.
        apply H.
    - apply Respects_StrongSubset_extendVarSetList.
      apply H0.
   * repeat apply Respects_StrongSubset_and; try apply Respects_StrongSubset_const.
     - apply H.
     - setoid_rewrite Forall'_Forall.
       apply Respects_StrongSubset_forall.
       rewrite Forall_forall.
       intros [[dc pats] rhs] HIn.
       repeat apply Respects_StrongSubset_and; try apply Respects_StrongSubset_const.
       specialize (H0 _ _ _ HIn).
       apply Respects_StrongSubset_extendVarSetList.
       apply H0.
   * apply H.
   * unfold Respects_StrongSubset.
     move=> vs1 vs2 SS.
     move=> [WSE WST].
     split.
     eauto.
     eapply Respects_StrongSubset_WellScopedTickish; eauto.
   * apply Respects_StrongSubset_const.
   * apply Respects_StrongSubset_const.
Qed.

author: DavidFHCh

repo: Tesis-FTW

save_path: github-repos/coq/DavidFHCh-Tesis-FTW


text:
Load loadpath.
Require Import Coq.Lists.List.
Require Import veristar.variables veristar.datatypes.
Require Import Coqlib.
Require Import VST.msl.Coqlib2.
Require Import ZArith.
Require Import veristar.compare.
Require Import veristar.clauses.

Fixpoint freshmax_expr (e: expr) : var :=
  match e with
  | Nil => minid
  | Var v => v
  end.

Definition var_max (x y : var) : var :=
 match Ident.compare x y with Lt => y | _ => x end.

Definition freshmax_pn_atom (a: pn_atom) : var :=
  match a with
  | Equ e1 e2 => var_max (freshmax_expr e1) (freshmax_expr e2)
  | Nequ e1 e2 => var_max (freshmax_expr e1) (freshmax_expr e2)
  end.

Definition freshmax_space_atom (a: space_atom) : var :=
  match a with
  | Next e1 e2 =>  var_max (freshmax_expr e1) (freshmax_expr e2)
  | Lseg e1 e2 =>  var_max (freshmax_expr e1) (freshmax_expr e2)
 end.

Definition freshmax_list {A} (f: A -> var) (l: list A) : var :=
  fold_right (fun a i => var_max (f a) i) minid l.

Definition freshmax_assertion (a: assertion) : var :=
  match a with
  | Assertion pi sigma =>
     var_max (freshmax_list freshmax_pn_atom pi)
            (freshmax_list freshmax_space_atom sigma)
  end.

Definition freshmax_pure_atom (a: pure_atom) : var :=
  match a with
  | Eqv e1 e2 => var_max (freshmax_expr e1) (freshmax_expr e2)
  end.

Definition freshmax_clause (c : clause) : var :=
 match c with
 | PureClause pi pi' _ _ =>  var_max (freshmax_list freshmax_pure_atom pi)
                                     (freshmax_list freshmax_pure_atom pi')
 | PosSpaceClause pi pi' sigma =>
     var_max (var_max (freshmax_list freshmax_pure_atom pi)
                                     (freshmax_list freshmax_pure_atom pi'))
                       (freshmax_list freshmax_space_atom sigma)
 | NegSpaceClause pi sigma pi' =>
     var_max (var_max (freshmax_list freshmax_pure_atom pi)
                                     (freshmax_list freshmax_pure_atom pi'))
                       (freshmax_list freshmax_space_atom sigma)
 end.

Lemma varmax_minid: forall x, var_max minid x = x.
Proof.
intros; unfold var_max.
id_compare minid x; auto.
apply minid_min in l; contradiction.
Qed.

Lemma varmax_minid': forall x, var_max x minid = x.
Proof.
intros; unfold var_max.
id_compare x minid; auto.
apply minid_min in l; contradiction.
Qed.

Lemma var_max_intro:
  forall a b c, Ident.lt a c -> Ident.lt b c -> Ident.lt (var_max a b) c.
Proof.
unfold var_max; intros; auto.
id_compare a b; auto.
Qed.

Lemma Ile_var_max1:  forall a b, Ile a (var_max a b).
Proof.
intros.
 unfold Ile, var_max.
 id_compare a b; subst; auto;  right; apply Ident.eq_equiv.
Qed.

Lemma Ile_var_max2:  forall a b, Ile b (var_max a b).
Proof.
intros.
 unfold Ile, var_max.
 id_compare a b; subst; auto;  right; apply Ident.eq_equiv.
Qed.

Lemma Ile_trans: forall a b c, Ile a b -> Ile b c -> Ile a c.
Proof.
 unfold Ile; intros.
 destruct H. left; destruct H0. eapply Ilt_trans; eauto.
 rewrite <- H0; auto. rewrite H in *; auto.
Qed.

Lemma Ile_minid: forall m, Ile minid m.
Proof.
 unfold Ile; intros.
 id_compare minid m. subst. right; apply Ident.eq_equiv.
 auto. apply minid_min in l; contradiction.
Qed.

Lemma var_max_intro':
  forall a b c, Ile a c -> Ile b c -> Ile (var_max a b) c.
Proof.
unfold var_max; intros; auto.
id_compare a b; auto.
Qed.

Lemma var_max_split': forall a b c, Ile (var_max a b) c -> Ile a c /\ Ile b c.
Proof.
unfold var_max; intros.
id_compare a b; subst; intuition.
destruct H. left; eapply Ilt_trans; eauto.
rewrite H in *. left; auto.
destruct H.
left; eapply Ilt_trans; eauto.
rewrite H in *.
left; auto.
Qed.

Lemma id_compare_refl: forall z, Ident.compare z z = Eq.
Proof. intro. id_compare z z; auto; contradiction (Ilt_irrefl l).
Qed.

Lemma id_compare_lt: forall x y, Ident.lt x y -> Ident.compare x y = Lt.
Proof. intros. id_compare x y; auto. subst; contradiction (Ilt_irrefl H).
contradiction (Ilt_irrefl (Ilt_trans H l)).
Qed.

Lemma id_compare_gt: forall x y, Ident.lt y x -> Ident.compare x y = Gt.
Proof. intros. id_compare x y; auto. subst; contradiction (Ilt_irrefl H).
contradiction (Ilt_irrefl (Ilt_trans l H)).
Qed.

Lemma var_max_assoc: forall x y z, var_max x (var_max y z) = var_max (var_max x y) z.
Proof.
intros.
unfold var_max.
id_compare x y.
subst. id_compare y z. subst.
rewrite id_compare_refl; auto.

rewrite id_compare_lt; auto.
rewrite id_compare_refl; auto.
id_compare y z; auto. subst. rewrite id_compare_lt; auto.
rewrite id_compare_lt; auto. eapply Ilt_trans; eauto.
id_compare x y; auto.
contradiction (Ilt_irrefl (Ilt_trans l1 l)).
id_compare y z; auto.
subst.
rewrite id_compare_gt; auto.
rewrite id_compare_gt; auto.
rewrite id_compare_gt; auto.
eapply Ilt_trans; eauto.
Qed.

Lemma var_max_com: forall x y, var_max x y = var_max y x.
Proof.
intros.
unfold var_max.
id_compare x y; auto.
subst; rewrite id_compare_refl; auto.
rewrite id_compare_gt; auto.
rewrite id_compare_lt; auto.
Qed.

Lemma var_max_split: forall a b c, Ident.lt (var_max a b) c -> Ident.lt a c /\ Ident.lt b c.
Proof.
unfold var_max; intros.
id_compare a b; subst; intuition.
transitivity b; auto.
transitivity a; auto.
Qed.

Lemma freshmax_list_app:
 forall {A} (f: A -> var) l1 l2,
    freshmax_list f (l1++l2) = var_max (freshmax_list f l1) (freshmax_list f l2).
Proof.
intros.
induction l1; simpl.
rewrite varmax_minid. auto.
rewrite IHl1.
rewrite var_max_assoc; auto.
Qed.

Lemma freshmax_list_rev:
 forall {A} (f: A -> var) l,
    freshmax_list f (rev l) = freshmax_list f l.
Proof.
induction l; simpl; auto.
rewrite freshmax_list_app.
rewrite IHl.
simpl.
rewrite (var_max_com (f a)).
rewrite varmax_minid.
apply var_max_com.
Qed.

Lemma Ile_freshmax_i3:
  forall s m,
    (forall x, M.In x s -> Ile (freshmax_clause x) m) ->
     Ile (freshmax_list freshmax_clause (M.elements s)) m.
Proof.
  intros.
  assert (forall x, List.In x (M.elements s) -> Ile (freshmax_clause x) m).
  intros. rewrite Melements_spec1 in H0. auto.
  clear H.
  revert H0; induction (M.elements s); simpl; intros.
  apply Ile_minid.
  apply var_max_intro'.
  apply H0; auto.
  apply IHl.
   intros; auto.
Qed.

Lemma merge_nil1:
  forall {A} (f: A -> A -> comparison) l, merge f nil l = l.
Proof.
 intros. induction l; simpl; auto.
Qed.

Lemma freshmax_list_merge:
  forall m al bl,
     Ile (freshmax_list freshmax_pure_atom al) m ->
     Ile (freshmax_list freshmax_pure_atom bl) m ->
     Ile (freshmax_list freshmax_pure_atom (merge pure_atom_cmp al bl)) m.
Proof.
 intros.
  revert bl H H0; induction al; simpl; intros; auto.
  revert H0; induction bl; simpl; intros; auto.
  apply var_max_split' in H; destruct H.
assert (IHal':
  forall bl, Ile (freshmax_list freshmax_pure_atom bl) m ->
       Ile (freshmax_list freshmax_pure_atom (merge pure_atom_cmp al bl)) m).
 intros; apply IHal; auto.
  clear IHal.
  revert H0; induction bl; intros.
  apply var_max_intro'; auto.
  apply var_max_split' in H0; destruct H0.
  destruct (pure_atom_cmp a a0).
  apply var_max_intro'; auto.
 apply IHal'; auto.
  apply var_max_intro'; auto.
  apply var_max_intro'; auto.
  apply IHal'.
  apply var_max_intro'; auto.
Qed.

Lemma Ile_freshmax_list:
  forall A (f: A -> var) m (s: list A),
    Ile (freshmax_list f s) m <-> (forall x, List.In x s -> Ile (f x) m).
Proof.
  intros.
  split; induction s; simpl; intros; try contradiction.
  destruct H0; subst.
  apply var_max_split' in H. destruct H; auto.
  apply var_max_split' in H. destruct H; auto.
  apply Ile_minid.
  simpl.
  apply var_max_intro'.
  apply H; simpl; auto.
  apply IHs; auto.
Qed.

Lemma freshmax_list_insu:
   forall A (f: A -> var) (cmp: A -> A -> comparison)
      (CMP_EQ: forall a b, a=b <-> Eq = cmp a b)
      a s,
      freshmax_list f (insert_uniq cmp a s) = var_max (f a) (freshmax_list f s).
Proof.
 induction s; simpl; intros; auto.
 case_eq (cmp a a0); intros.
 symmetry in H; apply CMP_EQ in H; subst a0.
 simpl.
 rewrite var_max_assoc.
 f_equal; auto.
 unfold var_max. destruct (Ident.compare (f a) (f a)); auto.
 simpl. rewrite IHs.
 repeat rewrite var_max_assoc.
 f_equal. apply var_max_com.
 simpl. auto.
Qed.

Lemma freshmax_list_sort:
  forall A (f: A -> var) (cmp: A -> A -> comparison)
      (CMP_EQ: forall a b, a=b <-> Eq = cmp a b)
      (s: list A),
    freshmax_list f (rsort_uniq cmp s) = freshmax_list f s.
Proof.
  induction s; simpl; intros; auto.
  rewrite freshmax_list_insu; auto.
  rewrite IHs; auto.
Qed.

Lemma freshmax_insu:
  forall m a pi,
       Ile (freshmax_pure_atom a) m ->
       Ile (freshmax_list freshmax_pure_atom pi) m ->
       Ile (freshmax_list freshmax_pure_atom
              (insert_uniq pure_atom_cmp a pi)) m.
Proof.
 intros. rewrite freshmax_list_insu; auto.
 apply var_max_intro'; auto.
Qed.

author: PrincetonUniversity

repo: VST