0

我想证明字符串的“自反性”属性。请如果你能帮助我如何进行证明。这是我的代码：

    Fixpoint beq_str (sa sb : String.string) {struct sb}: bool := 
   match sa, sb with
 | EmptyString, EmptyString  => true
 | EmptyString, String b sb' => false
 | String a sa', EmptyString => false
 | String a sa', String b sb'=> match (ascii_dec a b) with 
                                | left _ => beq_str sa' sb'
                                | right _ => false
                                end
 end.
 (* compares two string names [n1] and [n2] of type [id'] - returs bool. *) 
 Definition beq_names n1 n2 :=
  match (n1, n2) with
    (name s1, name s2) => beq_str s1 s2
  end.

 Theorem reflexivty : forall i,
  true = beq_str i i.
Proof.
  intros. induction i.
  auto.  simpl. Admitted.
4

1 回答 1

1

不知道是家庭作业还是独立学习...

Theorem beq_str_refl : forall i,
  true = beq_str i i.
Proof.
  induction 0; simpl; try (rewrite <- IHi; case (ascii_dec a a));
  try reflexivity; intro C; elimtype False; apply C; reflexivity.
Qed.

这应该有效。

如果这是家庭作业并且你很懒惰，你的导师可能会拒绝这个。如果您想自己理解和证明它，那么您需要的构建块就在那里，只需将它拆开并在您当前的证明状态下扔掉碎片。

这个证明中有两件令人讨厌的事情。第一个是摆脱(ascii_dec a a). （案例分析a不起作用。）对整个事情（即(ascii_dec a a)）进行案例分析以获得两个子目标，一个带有添加的假设a = a，另一个带有a <> a。

第二个问题可能是处理矛盾，除非你以前做过。

a <> a相当于a = a -> False。 a = a根据定义为真，它允许构造一个类型的值False（矛盾——False没有构造函数）。这使您可以放弃当前的目标（true = false无论如何都无法证明），而只是构建那个不可能的False值。

告诉 Coq你elimtype False想继续对False. 由于False没有构造函数，这使您只有一个目标，即构造一个False. 通常这是不可能的，但你的假设之间存在矛盾。 apply这个矛盾（C在我上面的证明脚本中命名）和你剩下要做的就是 show a = a，它来自reflexivity.

这是一个更易读的版本，您可以逐步完成：

Theorem beq_str_refl : forall i, true = beq_str i i.
  intro i. induction i as [ | a i IHi ].
    (* base case: Empty String *) reflexivity.
    (* inductive case: *) simpl. rewrite <- IHi.
      (* do case analysis on ascii_dec (or {a=a}+{a<>a}) *)
      destruct (ascii_dec a a) as [ Heq | C ].
      (* {a =  a} *) reflexivity.
      (* {a <> a} *) unfold not in C. elimtype False. apply C. reflexivity.

另一种处理矛盾的方法：

(* just a quick nonsensical goal *)
Theorem foo: forall i, i <> i -> 2 + 2 = 5.
  intros i C.
  (* explicitly construct a 'False' value *)
  assert False as H.
    apply C. reflexivity.
  (* 'inversion' generates one goal per possible constructor *)
  (* as False has no constructors, this gives 0 subgoals, finishing the proof *)
  inversion H.
Qed.
于 2012-07-09T19:58:51.280 回答