0

私は Coq の初心者で、行き止まりに遭遇しました。おおよそ次のような帰納的な定義があります (前に帰納的に受け入れを定義しました)。

Inductive fun : accepts -> Prop :=
  | fn1 : fun True
  | fn2 : forall (n : nat )(A : accepts), fun A -> fun (n A).

私が証明する必要があるのはこれです：

Lemma lem_1  (A : formula) (n : nat) (h : fun (n A)) : fun A.

もちろん、私が得る証明を開始するとき

 A : accepts
 n : nat
 h : fun (n A)
 ============================
 fun A

私は長い間戦術について読んで、h を fn2 などにプラグインできる方法を見つけようとしましたが、それを行う方法を見つけることができません。誰かが私をここに案内して、アイデアを教えてもらえますか?? また、楽しい A を A に単純化するために何かをしようとしましたが、そこでも成功しませんでした。ご助力ありがとうございます！

4

1 に答える 1

1

hあなたは自分の仮説がfn2ルールを使用して作成されたと主張したいようです。Coq の専門用語では、これにはその仮説を逆転させる必要があります。これを行うには、 を呼び出すことができますinversion h。適用は逆のプロセスです: ルールを導出するfn2ことを示す仮説と組み合わせます。fun Afun (n A)

于 2016-03-10T21:22:21.883 に答える