Reasoning

Click on a command or tactic to see a detailed view of its use.

% Define constructors for mappings
Kind map type -> type -> type.
Type map    A -> B -> map A B.

% Substitution encoded as a relation
% such that (subst L M M') holds if and only if
% M' is the result of applying the substitution L to M.
Define subst : list (map A A) -> B -> B -> prop by
  subst nil M M;
  nabla x, subst (map x V :: ML) (R x) M :=
    subst ML (R V) M.

% Substitution is deterministic
Theorem subst_det[A,B] : forall (ML:list (map A A)) (M:B) M' M'',
  subst ML M M' -> subst ML M M'' -> M' = M''.
induction on 1. intros. case H1.
  case H2. search.
  case H2. apply IH to H3 H4. search.
% Pruning vacuous occurrences of variables in the results of substitutions
Theorem subst_prune[A,B,C] : 
  forall (ML:list (map A A)) (M:B) M', nabla (x:C),
  subst ML M (M' x) -> exists M'', M' = y\M''.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.
 
% An instantiation lemma for substitution
Theorem subst_inst[A,B,C] : 
  forall (ML:list (map A A)) (M1:C) (M2:C -> B) M1' M2', nabla (x:C),
  subst ML M1 M1' -> subst ML (M2 x) (M2' x) -> 
    subst ML (M2 M1) (M2' M1').
induction on 2. intros. case H2.
  case H1. search.
  case H1. apply IH to H4 H3. search.