0

Assume I have the following Set:

Inductive Many : Set := 
| aa: Many
| bb: Many
| cc: Many
(* | ... many more constructors *)
.

How can I proof in the _ match, that y<>aa?

match x with
| aa     => true
| _ as y => (* how can i proof that y <> aa ? *)
4

1 回答 1

1

不幸的是，如果没有更多的纯加利纳工作，似乎不可能得到这样的证明。你想写的是：

  match x with
  | aa => true
  | y =>
    let yNOTaa : y <> aa := fun yaa =>
      eq_ind y (fun e => match e with aa => False | _ => True end) I aa yaa
    in false
  end

但这在 Gallina 中效果不佳，因为它不会将通配符扩展到所有可能的情况，从而y在eq_ind调用中留下抽象。然而，它确实在战术模式下工作：

refine (
  match x with
  | aa => true
  | y =>
    let yNOTaa : y <> aa := fun yaa =>
      eq_ind y (fun e => match e with aa => False | _ => True end) I aa yaa
    in false
  end
).

但它实际上用所有分支构建了扩展术语。

我刚刚发现有一种方法可以让 Vernacular 构建与细化策略构建的术语相同的术语。为此，您必须强制返回提及被歧视者的注释，如下所示：

Definition foo (x : many) : bool :=
  match x return (fun _ => bool) x with
  | aa => true
  | y =>
    let yNOTaa : y <> aa := fun yaa : y = aa =>
      @eq_ind many y (fun e => match e with aa => False | _ => True end) I aa yaa
    in false
  end
.

我的猜测是，无论匹配是否依赖，详细说明一词都会有所不同...

于 2013-10-09T21:24:29.590 回答