Generi c равенство подъема в к

Question

Есть ли какие-либо такты c или факт или что-то еще, чтобы поднять равенство в конструктор индуктивного и обратного, вывести равенство индуктивных конструкторов в равенство аргументов конструктора, то есть:

forall T: Type, forall t1 t2: T, Some t1 = Some t2 -> t1 = t2 
forall T: Type, forall t1 t2: T, t1 = t2 -> Some t1 = Some t2 

Answer 1

Первый принцип обычно известен как инъективность конструкторов, и есть несколько тактов c, которые могут его использовать. Одним из вариантов является injection tacti c:

Goal forall T: Type, forall t1 t2: T, Some t1 = Some t2 -> t1 = t2.
intros T t1 t2 H. injection H as H. apply H.
Qed.

Другой принцип действителен для любой функции, а не только для конструкторов. Вы можете использовать f_equal tacti c:

Goal forall T: Type, forall t1 t2: T, t1 = t2 -> Some t1 = Some t2.
intros T t1 t2 H. f_equal. exact H.
Qed.

. Обратите внимание, что в этой ситуации часто проще просто переписать с равенством, так как это позволяет избежать создания нескольких целей, когда у вас есть несколько аргументов функция:

Goal forall T: Type, forall t1 t2: T, t1 = t2 -> Some t1 = Some t2.
intros T t1 t2 H. rewrite H. trivial.
Qed.