使用 let-in 调用定理

Question

我有一个函数 f 返回一对。然后我证明了一些关于它的结果。 在我的引理中，我第一次尝试获取每个组件是使用let (x, y) := f z in。但是，尝试使用这些引理似乎很麻烦。 apply 不能直接工作，我必须使用 pose proof 或其变体在假设中添加引理并破坏 f z 才能使用它。有没有办法在引理中顺利使用 let-in ？还是因为使用起来很痛苦而气馁？

为了完成我的问题，这里是我写关于f 的引理的其他尝试。我尝试直接使用fst (f z) 和snd (f z)，但我也发现它很麻烦。最后，我以forall x y, (x,y) = f z -> 开始了我的引理。

这是一个具体的例子。

Require Import List. Import ListNotations.

Fixpoint split {A} (l:list A) :=
  match l with
  | [] => ([], [])
  | [a] => ([a], [])
  | a::b::l => let (l1, l2) := split l in (a::l1, b::l2)
  end.

Lemma split_in : forall {A} (l:list A) x,
  let (l1, l2) := split l in 
  In x l1 \/ In x l2 <-> In x l.

Lemma split_in2 : forall {A} (l:list A) x,
  In x (fst (split l)) \/ In x (snd (split l)) <-> In x l.

Lemma split_in3 : forall {A} (l:list A) x l1 l2,
  (l1, l2) = split l ->
  In x l1 \/ In x l2 <-> In x l.

Answer 1

您已经找到了我认为正确的解决方案。 let (l1, l2) := ... in ... 将阻止减少并破坏一切。使用split_in2 还是split_in3 取决于你的出发点是什么。

但是请注意，打开Primitive Projections 并将prod 重新定义为原始记录将使split_in 和split_in2 实际上是相同的定理，因为split l 和(fst (split l), snd (split l)) 是判断性的平等的。你可以这样做

Set Primitive Projections.
Record prod {A B} := pair { fst : A ; snd : B }.
Arguments prod : clear implicits.
Arguments pair {A B}.
Add Printing Let prod.
Notation "x * y" := (prod x y) : type_scope.
Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
Hint Resolve pair : core.