(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Max Omega Wellfounded.

From Undecidability.Shared.Libs.DLW.Utils
  Require Import utils.

Set Implicit Arguments.

Reserved Notation " e '⇢' x " (at level 58).
Reserved Notation " e [ v / x ] " (at level 57, v at level 0, x at level 0, left associativity).
Reserved Notation " e ⦃  x '⇠' v ⦄ " (at level 57, v at level 0, x at level 0, left associativity).

Section env.

  Variable (X Y : Type) (X_eq_dec : eqdec X) (Y_default : Y).
  
  Definition env := X -> Y.
  
  Implicit Type e : env.

  Definition get_env e x := e x.
    
  Definition set_env e x v : env := fun y => if X_eq_dec x y then v else e y.
  
  Definition nil_env : env := fun _ => Y_default.
  
  Fact get_set_env_eq e v p q : p = q -> get_env (set_env e p v) q = v.
  Proof. intros []; unfold set_env, get_env; destruct (X_eq_dec p p) as [ | [] ]; auto. Qed.
  
  Fact get_set_env_neq e v p q : p <> q -> get_env (set_env e p v) q = get_env e q.
  Proof. simpl; intros H; unfold set_env, get_env; destruct (X_eq_dec p q); auto; destruct H; auto. Qed.
  
End env.

Arguments nil_env {X}.

Opaque get_env.
Opaque set_env.

Local Notation " e ⇢ x " := (@get_env _ _ e x).
Local Notation " e ⦃  x ⇠ v ⦄ " := (@set_env _ _ _ e x v).

(* find the value of x inside the environment t *)

Ltac find_val x t :=
  match t with
    | ?s⦃x⇠?v⦄ => v
    | ?s⦃_⇠_⦄ => find_val x s
  end.

Tactic Notation "rew" "env" :=
  repeat lazymatch goal with 
    |              |- context[ _⦃ ?x⇠_⦄⇢?x ] => rewrite get_set_env_eq  with (1 := eq_refl x)
    | _ : ?x = ?y  |- context[ _⦃ ?x⇠_⦄⇢?y ] => rewrite get_set_env_eq  with (p := x) (q := y)
    | _ : ?y = ?x  |- context[ _⦃ ?x⇠_⦄⇢?y ] => rewrite get_set_env_eq  with (p := x) (q := y)
    | _ : ?x <> ?y |- context[ _⦃ ?x⇠_⦄⇢?y ] => rewrite get_set_env_neq with (p := x) (q := y)
    | _ : ?y <> ?x |- context[ _⦃ ?x⇠_⦄⇢?y ] => rewrite get_set_env_neq with (p := x) (q := y)
    |              |- context[ _⦃ ?x⇠_⦄⇢?y ] => rewrite get_set_env_neq with (p := x) (q := y);
                                                  [ | discriminate ]
  end; auto.

(*
Tactic Notation "rew" "envi" :=
  repeat lazymatch goal with 
    | |- context f[ _[_/?l]#>?l ] => rewrite get_set_env_eq with (x := l) 
    | _ : ?l <> ?m |- context f[ _[_/?l]#>?m ] => rewrite get_set_env_neq with (x := l) (y := m)
    | _ : ?m <> ?l |- context f[ _[_/?l]#>?m ] => rewrite get_set_env_neq with (x := l) (y := m)
    | |- context f[ _[_/?l]#>?m ] => rewrite get_set_env_neq with (x := l) (y := m); [ | discriminate ]
  end; auto.
*)

Tactic Notation "rew" "env" "in" hyp(H) := revert H; rew env; intros H.