Договаривающееся вложенными пусть statments

Question

На данный момент у меня есть случай индукции, как это (усеченного другая информация, как введенные переменные, я могу добавить его в случае необходимости):

IHe : not_set e -> (let (a, _) := sem e c in a) = c 
    ============================ 
    (let (a, _) := let (c0, r) := sem e c in (c0, - r) in a) = c 

Я действительно не использовал let ключевое слово много (на самом деле, я использовал один случай match, который Coq казался автоматически псевдонимом let). Однако, это кажется довольно очевидным, что утверждение:

(let (a, _) := let (c0, r) := sem e c in (c0, - r) in a) 

ли просто альясинга те же значения, с несколькими уровнями косвенности. То есть, a=c0=c0 и _=-r=r, но я не могу понять, как это уменьшить. Я уже пробовал такие вещи, как simpl и auto. Я столкнулся с cbv zeta, который, как я понимаю, должен упростить let заявления, но ничего не сделал.

Что мне здесь не хватает? Я подумал о том, чтобы ввести лемму, но без возможности договориться, давайте вообще не знаю, что я хотел бы доказать. (Значение: если бы я мог доказать все, что могло бы помочь, мне не понадобилось бы доказывать).

Answer 1

Вам необходимо посмотреть на результат sem e c.

destruct (sem e c) eqn:?. simpl in *. 

Это также можно доказать

(let (a, _) := let (c0, r) := sem e c in (c0, - r) in a) = (let (a, _) := sem e c in a), 

снова, проверив пару, так как второй элемент пары не используется.