Set Implicit Arguments.
Require Import List.
Require Import MyTactics.
Require Import Types.
Require Import TypeEquality.
Require Import MoreTypeEquality.
-------------------------------------------------------------------------
Tactics for proving type equality goals, while exploiting the equational
theory of tensor. (Because tyeq is not intensional equality, we cannot
use autorewrite.)
eqth_step assumes that the goal is the form tyeq (TyTensor _ _) _, and
tries to solve it using a single law of the equational theory. If the
right-hand side is a unification variable, it is instantiated.
Ltac eqth_step :=
first [
eapply tyeq_tensor_arrow
|
eapply tyeq_tensor_pair
|
eapply tyeq_tensor_unit
|
eapply tyeq_tensor_q
|
eapply tyeq_tensor_bang
|
eapply tyeq_tensor_ref
|
eapply tyeq_tensor_at
|
eapply tyeq_tensor_regioncap
|
eapply tyeq_tensor_regioncappunched
|
eapply tensor_subst
];
wf.
TEMPORARY instead of this costly disjunction, one could/should use the lemma tyred_tyeq directly
eqth assumes that the goal is the form tyeq (TyTensor _ _) _, and tries
to solve it using at least one step, and as many steps as possible, in the
equational theory.
Ltac eqth :=
eapply tyeq_transitive; [
eqth_step |
prove_tyeq |
wf ]
prove_tyeq attempts to prove the goal, if it is of the form tyeq _ _
or wf _. It simplifies applications of tensor.
with prove_tyeq :=
match goal with
First, try exploiting the equational theory.
| |-
tyeq (
TyTensor _ _)
_ =>
eqth
| |-
tyeq _ (
TyTensor _ _) =>
eapply tyeq_symmetric;
eqth
Otherwise, try decomposing the goal; instantiate unification variables
if required. If decomposition does not work, try reflexivity.
| |-
tyeq _ _ =>
first [
eapply tyeq_var
|
eapply tyeq_arrow
|
eapply tyeq_pair
|
eapply tyeq_q
|
eapply tyeq_bang
|
eapply tyeq_ref
|
eapply tyeq_region
|
eapply tyeq_at
|
eapply tyeq_regioncap
|
eapply tyeq_regioncappunched
|
eapply tyeq_reflexive
];
prove_tyeq
If this is a well-formedness goal, kill it.
| |-
wf _ =>
wf
If none of this works, give up.
|
_ =>
idtac
end.
tyeq_under_tensor attempts to work under a tensor. If both sides of the
goal exhibit a tensor, then tyeq_tensor is applied in order to work under
the tensor. If only the left-hand side of the goal exhibits a tensor, then
transitivity is invoked, and tyeq_tensor is applied on the left-hand
side, in order to again work under the tensor.
Ltac tyeq_under_tensor :=
match goal with
| |-
tyeq (
TyTensor _ ?
u) (
TyTensor _ ?
u) =>
eapply tyeq_tensor; [
idtac |
eapply tyeq_reflexive;
wf ]
| |-
tyeq (
tensors _ ?
us) (
tensors _ ?
us) =>
eapply tyeq_tensors; [
wf |
idtac ]
| |-
tyeq (
TyTensor _ _)
_ =>
eapply tyeq_transitive; [
eapply tyeq_tensor; [
idtac |
eapply tyeq_reflexive;
wf ] |
idtac |
idtac ]
| |-
tyeq (
tensors _ _)
_ =>
eapply tyeq_transitive; [
eapply tyeq_tensors; [
wf |
idtac ] |
idtac |
idtac ]
end.