LibSepVarAppendix - Program Variables

Set Implicit Arguments.
From SLF Require LibListExec.
From SLF Require Export LibString LibList LibCore.
From SLF Require Import LibSepFmap LibSepTLCbuffer.
Open Scope string_scope.
Generalizable Variables A.

Representation of Program Variables

This file contains definitions, lemmas, tactics and notations for manipulating program variables and list of program variables.

Representation of Variables

Variables are represented as strings
Definition var : Type := string.
The boolean function var_eq s1 s2 compares two variables.
Definition var_eq (s1:var) (s2:var) : bool :=
  if String.string_dec s1 s2 then true else false.
The boolean function var_eq s1 s2 returns true iff the equality v1 = v2 holds.
Lemma var_eq_spec : ∀ s1 s2,
  var_eq s1 s2 = isTrue (s1 = s2).
Proof using.
  intros. unfold var_eq. case_if; rew_bool_eq¬.
Qed.
Global Opaque var.

Tactic case_var

The tactic case_var performs case analysis on expressions of the form if var_eq x y then .. else .. that appear in the goal.
Tactic Notation "case_var" :=
  repeat rewrite var_eq_spec in *; repeat case_if.
Tactic Notation "case_var" "~" :=
  case_var; auto_tilde.
Tactic Notation "case_var" "*" :=
  case_var; auto_star.

Representation of List of Variables

Definition of Distinct Variables

vars is the type of a list of variables
Definition vars : Type := list var.
var_fresh y xs asserts that y does not belong to the list xs
Fixpoint var_fresh (y:var) (xs:vars) : bool :=
  match xs with
  | nil ⇒ true
  | x::xs' ⇒ if var_eq x y then false else var_fresh y xs'
  end.
var_distinct xs asserts that xs consists of a list of pairwise distinct variables, i.e., a list of variables distinct from each other.
Fixpoint var_distinct (xs:vars) : Prop :=
  match xs with
  | nil ⇒ True
  | x::xs' ⇒ var_fresh x xs' ∧ var_distinct xs'
  end.
var_distinct_exec xs is a boolean function that decides whether a list of variables contains only distinct variables, that is, whether the proposition var_distinct xs is satisfied.
Fixpoint var_distinct_exec (xs:vars) : bool :=
  match xs with
  | nil ⇒ true
  | x::xs' ⇒ var_fresh x xs' && var_distinct_exec xs'
  end.
Lemma var_distinct_exec_eq : ∀ xs,
  var_distinct_exec xs = isTrue (var_distinct xs).
Proof using.
  intros. induction xs as [|x xs']; simpl; rew_isTrue.
  { auto. } { rewrite¬IHxs'. }
Qed.
The following lemma asserts that if x is a variable in the list xs, and y is fresh from this list xs, then y is not equal to x.
Lemma var_fresh_mem_inv : ∀ y x xs,
  var_fresh x xs →
  mem y xs →
  x ≠ y.
Proof using.
  introv H M N. subst. induction xs as [|x xs'].
  { inverts M. }
  { simpls. case_var. inverts¬M. }
Qed.

Definition of n Distinct Variables

var_funs xs n asserts that xs consists of n distinct variables, where n is asserted to be a postive number.
Definition var_funs (xs:vars) (n:nat) : Prop :=
     var_distinct xs
  ∧ length xs = n
  ∧ xs ≠ nil.
var_funs xs n is a boolean function that decides whether the proposition var_funs xs n is satisfied
Definition var_funs_exec (xs:vars) (n:nat) : bool :=
     LibNat.beq n (LibListExec.length xs)
  && LibListExec.is_not_nil xs
  && var_distinct_exec xs.
Lemma var_funs_exec_eq : ∀ (n:nat) xs,
  var_funs_exec xs n = isTrue (var_funs xs n).
Proof using.
  intros. unfold var_funs_exec, var_funs.
  rewrite LibNat.beq_eq.
  rewrite LibListExec.is_not_nil_eq.
  rewrite LibListExec.length_eq.
  rewrite var_distinct_exec_eq.
  extens. rew_istrue. iff*.
Qed.

Generation of n Distinct Variables

nat_to_var n converts nat values into distinct name values.
Definition dummy_char :=
  Ascii.ascii_of_nat 0%nat.
Fixpoint nat_to_var (n:nat) : var :=
  match n with
  | O ⇒ String.EmptyString
  | S n' ⇒ String.String dummy_char (nat_to_var n')
  end.
Lemma injective_nat_to_var :
  injective nat_to_var.
Proof using.
  intros n. induction n as [|n']; intros m E; destruct m as [|m']; tryfalse.
  { auto. }
  { inverts E. fequals¬. }
Qed.
var_seq i n generates a list of variables x1;x2;..;xn with x1=i and xn=i+n-1. The ability to start at a given offset is sometimes useful.
Fixpoint var_seq (start:nat) (nb:nat) : vars :=
  match nb with
  | O ⇒ nil
  | S nb' ⇒ (nat_to_var start) :: var_seq (S start) nb'
  end.
The properties of var_seq are stated next. They assert that this function produce the expected number of variables, that the variables are pairwise distinct
Section Var_seq.
Implicit Types start nb : nat.
Lemma var_fresh_var_seq_lt : ∀ (x:nat) start nb,
  (x < start)%nat →
  var_fresh (nat_to_var x) (var_seq start nb).
Proof using.
  intros. gen start. induction nb; intros.
  { auto. }
  { simpl. case_var.
    { lets: injective_nat_to_var C. math. }
    { applys IHnb. math. } }
Qed.
Lemma var_fresh_var_seq_ge : ∀ (x:nat) start nb,
  (x ≥ start+nb)%nat →
  var_fresh (nat_to_var x) (var_seq start nb).
Proof using.
  intros. gen start. induction nb; intros.
  { auto. }
  { simpl. case_var.
    { lets: injective_nat_to_var C. math. }
    { applys IHnb. math. } }
Qed.
Lemma var_distinct_var_seq : ∀ start nb,
  var_distinct (var_seq start nb).
Proof using.
  intros. gen start. induction nb; intros.
  { simple¬. }
  { split.
    { applys var_fresh_var_seq_lt. math. }
    { auto. } }
Qed.
Lemma length_var_seq : ∀ start nb,
  length (var_seq start nb) = nb.
Proof using.
  intros. gen start. induction nb; simpl; intros.
  { auto. } { rew_list. rewrite¬IHnb. }
Qed.
Lemma var_funs_var_seq : ∀ start nb,
  (nb > 0%nat)%nat →
  var_funs (var_seq start nb) nb.
Proof using.
  introv E. splits.
  { applys var_distinct_var_seq. }
  { applys length_var_seq. }
  { destruct nb. { false. math. } { simpl. auto_false. } }
Qed.
End Var_seq.

Notation for Program Variables

When writing deeply-embedded programs, it is nice to write identifiers (program variables) without quotes. In the future, the "Custom Entry" mechanism might allow for this in a generic manner. In the meantime, we need one definition or one notation for each identifier

Program Variables Expressed Using Definitions

These definitions allowing to use the string notation "x" without any double quote or quotes. However, the scope of these definitions should be wrapped in a module to avoid clashes with local variables. E.g. Module Export Foo. Import DefinitionsForVariables. (...) End Foo.
Module DefinitionsForVariables.
Definition a := ("a":var).
Definition b := ("b":var).
Definition c := ("c":var).
Definition d := ("d":var).
Definition e := ("e":var).
Definition f := ("f":var).
Definition g := ("g":var).
Definition h := ("h":var).
Definition i := ("i":var).
Definition j := ("j":var).
Definition k := ("k":var).
Definition l := ("l":var).
Definition m := ("m":var).
Definition n := ("n":var).
Definition o := ("o":var).
Definition p := ("p":var).
Definition q := ("q":var).
Definition r := ("r":var).
Definition s := ("s":var).
Definition t := ("t":var).
Definition u := ("u":var).
Definition v := ("v":var).
Definition w := ("w":var).
Definition x := ("x":var).
Definition y := ("y":var).
Definition z := ("z":var).
Definition a1 := ("a1":var).
Definition b1 := ("b1":var).
Definition c1 := ("c1":var).
Definition d1 := ("d1":var).
Definition e1 := ("e1":var).
Definition f1 := ("f1":var).
Definition g1 := ("g1":var).
Definition h1 := ("h1":var).
Definition i1 := ("i1":var).
Definition j1 := ("j1":var).
Definition k1 := ("k1":var).
Definition l1 := ("l1":var).
Definition m1 := ("m1":var).
Definition n1 := ("n1":var).
Definition o1 := ("o1":var).
Definition p1 := ("p1":var).
Definition q1 := ("q1":var).
Definition r1 := ("r1":var).
Definition s1 := ("s1":var).
Definition t1 := ("t1":var).
Definition u1 := ("u1":var).
Definition v1 := ("v1":var).
Definition w1 := ("w1":var).
Definition x1 := ("x1":var).
Definition y1 := ("y1":var).
Definition z1 := ("z1":var).
Definition a2 := ("a2":var).
Definition b2 := ("b2":var).
Definition c2 := ("c2":var).
Definition d2 := ("d2":var).
Definition e2 := ("e2":var).
Definition f2 := ("f2":var).
Definition g2 := ("g2":var).
Definition h2 := ("h2":var).
Definition i2 := ("i2":var).
Definition j2 := ("j2":var).
Definition k2 := ("k2":var).
Definition l2 := ("l2":var).
Definition m2 := ("m2":var).
Definition n2 := ("n2":var).
Definition o2 := ("o2":var).
Definition p2 := ("p2":var).
Definition q2 := ("q2":var).
Definition r2 := ("r2":var).
Definition s2 := ("s2":var).
Definition t2 := ("t2":var).
Definition u2 := ("u2":var).
Definition v2 := ("v2":var).
Definition w2 := ("w2":var).
Definition x2 := ("x2":var).
Definition y2 := ("y2":var).
Definition z2 := ("z2":var).
Definition a3 := ("a3":var).
Definition b3 := ("b3":var).
Definition c3 := ("c3":var).
Definition d3 := ("d3":var).
Definition e3 := ("e3":var).
Definition f3 := ("f3":var).
Definition g3 := ("g3":var).
Definition h3 := ("h3":var).
Definition i3 := ("i3":var).
Definition j3 := ("j3":var).
Definition k3 := ("k3":var).
Definition l3 := ("l3":var).
Definition m3 := ("m3":var).
Definition n3 := ("n3":var).
Definition o3 := ("o3":var).
Definition p3 := ("p3":var).
Definition q3 := ("q3":var).
Definition r3 := ("r3":var).
Definition s3 := ("s3":var).
Definition t3 := ("t3":var).
Definition u3 := ("u3":var).
Definition v3 := ("v3":var).
Definition w3 := ("w3":var).
Definition x3 := ("x3":var).
Definition y3 := ("y3":var).
Definition z3 := ("z3":var).
Tactic to unfold these definitions. Useful to avoid the definitions to get in the way of simpl.
Ltac libsepvar_unfold :=
  unfold
  a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z,
  a1, b1, c1, d1, e1, f1, g1, h1, i1, j1, k1, l1, m1, n1, o1, p1, q1, r1, s1, t1, u1, v1, w1, x1, y1, z1,
  a2, b2, c2, d2, e2, f2, g2, h2, i2, j2, k2, l2, m2, n2, o2, p2, q2, r2, s2, t2, u2, v2, w2, x2, y2, z2,
  a3, b3, c3, d3, e3, f3, g3, h3, i3, j3, k3, l3, m3, n3, o3, p3, q3, r3, s3, t3, u3, v3, w3, x3, y3, z3.
End DefinitionsForVariables.

Program Variables Expressed Using Notation, with a Quote Symbol

To avoid using the string notation "x" for refering to a variable called x, one can use the notation 'x, available by importing the following module.
Declare Custom Entry trm.
Module NotationForVariables.
Declare Scope trm_scope.
Notation "''a'" := ("a":var) (in custom trm at level 0) : trm_scope.
Notation "''b'" := ("b":var) (in custom trm at level 0) : trm_scope.
Notation "''c'" := ("c":var) (in custom trm at level 0) : trm_scope.
Notation "''d'" := ("d":var) (in custom trm at level 0) : trm_scope.
Notation "''e'" := ("e":var) (in custom trm at level 0) : trm_scope.
Notation "''f'" := ("f":var) (in custom trm at level 0) : trm_scope.
Notation "''g'" := ("g":var) (in custom trm at level 0) : trm_scope.
Notation "''h'" := ("h":var) (in custom trm at level 0) : trm_scope.
Notation "''i'" := ("i":var) (in custom trm at level 0) : trm_scope.
Notation "''j'" := ("j":var) (in custom trm at level 0) : trm_scope.
Notation "''k'" := ("k":var) (in custom trm at level 0) : trm_scope.
Notation "''l'" := ("l":var) (in custom trm at level 0) : trm_scope.
Notation "''m'" := ("m":var) (in custom trm at level 0) : trm_scope.
Notation "''n'" := ("n":var) (in custom trm at level 0) : trm_scope.
Notation "''o'" := ("o":var) (in custom trm at level 0) : trm_scope.
Notation "''p'" := ("p":var) (in custom trm at level 0) : trm_scope.
Notation "''q'" := ("q":var) (in custom trm at level 0) : trm_scope.
Notation "''r'" := ("r":var) (in custom trm at level 0) : trm_scope.
Notation "''s'" := ("s":var) (in custom trm at level 0) : trm_scope.
Notation "''t'" := ("t":var) (in custom trm at level 0) : trm_scope.
Notation "''u'" := ("u":var) (in custom trm at level 0) : trm_scope.
Notation "''v'" := ("v":var) (in custom trm at level 0) : trm_scope.
Notation "''w'" := ("w":var) (in custom trm at level 0) : trm_scope.
Notation "''x'" := ("x":var) (in custom trm at level 0) : trm_scope.
Notation "''y'" := ("y":var) (in custom trm at level 0) : trm_scope.
Notation "''z'" := ("z":var) (in custom trm at level 0) : trm_scope.
Notation "''a1'" := ("a1":var) (in custom trm at level 0) : trm_scope.
Notation "''b1'" := ("b1":var) (in custom trm at level 0) : trm_scope.
Notation "''c1'" := ("c1":var) (in custom trm at level 0) : trm_scope.
Notation "''d1'" := ("d1":var) (in custom trm at level 0) : trm_scope.
Notation "''e1'" := ("e1":var) (in custom trm at level 0) : trm_scope.
Notation "''f1'" := ("f1":var) (in custom trm at level 0) : trm_scope.
Notation "''g1'" := ("g1":var) (in custom trm at level 0) : trm_scope.
Notation "''h1'" := ("h1":var) (in custom trm at level 0) : trm_scope.
Notation "''i1'" := ("i1":var) (in custom trm at level 0) : trm_scope.
Notation "''j1'" := ("j1":var) (in custom trm at level 0) : trm_scope.
Notation "''k1'" := ("k1":var) (in custom trm at level 0) : trm_scope.
Notation "''l1'" := ("l1":var) (in custom trm at level 0) : trm_scope.
Notation "''m1'" := ("m1":var) (in custom trm at level 0) : trm_scope.
Notation "''n1'" := ("n1":var) (in custom trm at level 0) : trm_scope.
Notation "''o1'" := ("o1":var) (in custom trm at level 0) : trm_scope.
Notation "''p1'" := ("p1":var) (in custom trm at level 0) : trm_scope.
Notation "''q1'" := ("q1":var) (in custom trm at level 0) : trm_scope.
Notation "''r1'" := ("r1":var) (in custom trm at level 0) : trm_scope.
Notation "''s1'" := ("s1":var) (in custom trm at level 0) : trm_scope.
Notation "''t1'" := ("t1":var) (in custom trm at level 0) : trm_scope.
Notation "''u1'" := ("u1":var) (in custom trm at level 0) : trm_scope.
Notation "''v1'" := ("v1":var) (in custom trm at level 0) : trm_scope.
Notation "''w1'" := ("w1":var) (in custom trm at level 0) : trm_scope.
Notation "''x1'" := ("x1":var) (in custom trm at level 0) : trm_scope.
Notation "''y1'" := ("y1":var) (in custom trm at level 0) : trm_scope.
Notation "''z1'" := ("z1":var) (in custom trm at level 0) : trm_scope.
Notation "''a2'" := ("a2":var) (in custom trm at level 0) : trm_scope.
Notation "''b2'" := ("b2":var) (in custom trm at level 0) : trm_scope.
Notation "''c2'" := ("c2":var) (in custom trm at level 0) : trm_scope.
Notation "''d2'" := ("d2":var) (in custom trm at level 0) : trm_scope.
Notation "''e2'" := ("e2":var) (in custom trm at level 0) : trm_scope.
Notation "''f2'" := ("f2":var) (in custom trm at level 0) : trm_scope.
Notation "''g2'" := ("g2":var) (in custom trm at level 0) : trm_scope.
Notation "''h2'" := ("h2":var) (in custom trm at level 0) : trm_scope.
Notation "''i2'" := ("i2":var) (in custom trm at level 0) : trm_scope.
Notation "''j2'" := ("j2":var) (in custom trm at level 0) : trm_scope.
Notation "''k2'" := ("k2":var) (in custom trm at level 0) : trm_scope.
Notation "''l2'" := ("l2":var) (in custom trm at level 0) : trm_scope.
Notation "''m2'" := ("m2":var) (in custom trm at level 0) : trm_scope.
Notation "''n2'" := ("n2":var) (in custom trm at level 0) : trm_scope.
Notation "''o2'" := ("o2":var) (in custom trm at level 0) : trm_scope.
Notation "''p2'" := ("p2":var) (in custom trm at level 0) : trm_scope.
Notation "''q2'" := ("q2":var) (in custom trm at level 0) : trm_scope.
Notation "''r2'" := ("r2":var) (in custom trm at level 0) : trm_scope.
Notation "''s2'" := ("s2":var) (in custom trm at level 0) : trm_scope.
Notation "''t2'" := ("t2":var) (in custom trm at level 0) : trm_scope.
Notation "''u2'" := ("u2":var) (in custom trm at level 0) : trm_scope.
Notation "''v2'" := ("v2":var) (in custom trm at level 0) : trm_scope.
Notation "''w2'" := ("w2":var) (in custom trm at level 0) : trm_scope.
Notation "''x2'" := ("x2":var) (in custom trm at level 0) : trm_scope.
Notation "''y2'" := ("y2":var) (in custom trm at level 0) : trm_scope.
Notation "''z2'" := ("z2":var) (in custom trm at level 0) : trm_scope.
Notation "''a3'" := ("a3":var) (in custom trm at level 0) : trm_scope.
Notation "''b3'" := ("b3":var) (in custom trm at level 0) : trm_scope.
Notation "''c3'" := ("c3":var) (in custom trm at level 0) : trm_scope.
Notation "''d3'" := ("d3":var) (in custom trm at level 0) : trm_scope.
Notation "''e3'" := ("e3":var) (in custom trm at level 0) : trm_scope.
Notation "''f3'" := ("f3":var) (in custom trm at level 0) : trm_scope.
Notation "''g3'" := ("g3":var) (in custom trm at level 0) : trm_scope.
Notation "''h3'" := ("h3":var) (in custom trm at level 0) : trm_scope.
Notation "''i3'" := ("i3":var) (in custom trm at level 0) : trm_scope.
Notation "''j3'" := ("j3":var) (in custom trm at level 0) : trm_scope.
Notation "''k3'" := ("k3":var) (in custom trm at level 0) : trm_scope.
Notation "''l3'" := ("l3":var) (in custom trm at level 0) : trm_scope.
Notation "''m3'" := ("m3":var) (in custom trm at level 0) : trm_scope.
Notation "''n3'" := ("n3":var) (in custom trm at level 0) : trm_scope.
Notation "''o3'" := ("o3":var) (in custom trm at level 0) : trm_scope.
Notation "''p3'" := ("p3":var) (in custom trm at level 0) : trm_scope.
Notation "''q3'" := ("q3":var) (in custom trm at level 0) : trm_scope.
Notation "''r3'" := ("r3":var) (in custom trm at level 0) : trm_scope.
Notation "''s3'" := ("s3":var) (in custom trm at level 0) : trm_scope.
Notation "''t3'" := ("t3":var) (in custom trm at level 0) : trm_scope.
Notation "''u3'" := ("u3":var) (in custom trm at level 0) : trm_scope.
Notation "''v3'" := ("v3":var) (in custom trm at level 0) : trm_scope.
Notation "''w3'" := ("w3":var) (in custom trm at level 0) : trm_scope.
Notation "''x3'" := ("x3":var) (in custom trm at level 0) : trm_scope.
Notation "''y3'" := ("y3":var) (in custom trm at level 0) : trm_scope.
Notation "''z3'" := ("z3":var) (in custom trm at level 0) : trm_scope.
End NotationForVariables.

Optional Material

Bonuse: the Tactic var_neq

This tactic is not used in the SLF volume.
The tactic var_neq helps prove calls of the form x ≠ y, where x and y are two concrete program variables. This tactic is registered as hint for auto
Ltac var_neq :=
  match goal with ⊢ ?x ≠ ?y :> var ⇒
    solve [ let E := fresh in
            destruct (String.string_dec x y) as [E|E];
              [ false | apply E ] ] end.
Hint Extern 1 (?x ≠ ?y) ⇒ var_neq.
(* 2022-09-20 16:51 *)