Module CanonicalValuesDoNotReduce

Set Implicit Arguments.
Require Import MyTactics.
Require Import Canonical.
Require Import SemanticsValues.

A sanity check: a canonical value does not reduce. This fact is actually unused.

Lemma canonical_values_do_not_reduce_preliminary:
(
  forall v1,
  canonical v1 ->
  forall v2,
  ~ redv v1 v2
) /\ (
  forall vs1,
  each_canonical vs1 ->
  forall vs2,
  ~ redvs vs1 vs2
).

Proof.

  apply canonical_induction; repeat intro;
  match goal with
  | h: redv _ _ |- _ => depelim h
  | h: redvs _ _ |- _ => depelim h
  end;
  intuition eauto.
Qed.

Definition canonical_values_do_not_reduce :=
proj1 canonical_values_do_not_reduce_preliminary.