使用让入调用定理 [英] Call a theorem using let-in

问题描述

我有一个函数 f 返回一对。然后我证明了一些结果。
在我的引理中，我第一次尝试获取每个组件的方法是使用 let（x，y）：= f z in 。但是，然后尝试使用这些引理似乎很麻烦。 apply 不能直接工作，我必须使用 pose证明或其变体在假设中添加引理销毁 fz 即可使用它。有没有一种方法可以在引理中顺利使用let-in？还是因为使用起来很痛苦而使它灰心？

I have a function f returning a pair. Then I prove some results about it. In my lemmas, my first attempt to get each component was using let (x, y) := f z in. But then, trying to use these lemmas seems cumbersome. apply does not work directly, I have to add the lemma in the hypothesis using pose proof or a variant of it and destruct f z to be able to use it. Is there a way to use let-in smoothly in lemmas ? Or is it discouraged because it is painful to use ?

为了完成我的问题，这是我为写关于 f 。我尝试直接使用 fst（f z）和 snd（f z），但是我也觉得很麻烦。最后，我以 forall xy，（x，y）= fz-> 开始我的引理。

To complete my question, here are the other attempts I made to write lemmas about f. I tried using fst (f z) and snd (f z) directly, but I also found it cumbersome. Finally, I started my lemmas with 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.

推荐答案

您已经找到了我认为是正确的解决方案。 let（l1，l2）：= ... in ... 将阻止还原并破坏所有内容。是使用 split_in2 还是 split_in3 取决于您的起点。

You have found what I believe is the correct solution. let (l1, l2) := ... in ... will block reduction and break everything. Whether you use split_in2 or split_in3 depends on what your starting point is.

但是请注意，打开原始投影并将 prod 重新定义为原始记录将使其生效因此 split_in 和 split_in2 实际上是相同的定理，因为 split l 和（fst（split l），snd（split l））在判断上是相等的。您可以使用

Note, however, that turning on Primitive Projections and redefining prod as a primitive record will make it so that split_in and split_in2 are actually the same theorem, because split l and (fst (split l), snd (split l)) are judgmentally equal. You can do this with

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.

这篇关于使用让入调用定理的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！