Coq
coqide

「Coqの余帰納法でハマってしまった」を記録

「Coqの余帰納法でハマってしまった」
https://qiita.com/Nogikuchi/items/28f2f573537ff3e5aca5
の1行づつの実行を coqide 8.7.1で記録してみた。
将来説明を追記。

余再帰呼び出しの結果をコンストラクタで包めばいいというわけではなく

Inductive List := Nil : List | Cons : nat -> List -> List.
Fixpoint length l :=
  match l with
  | Nil => O
  | Cons n l' => S (length l') (* l' は l より "小さい" *)
  end.

CoInductive Stream := SCons : nat -> Stream -> Stream.
CoFixpoint countup (n : nat) : Stream :=
  SCons n (countup (S n)). 
(*SCons n (countup (S n)) は (countup (S n)) より大きい*)

CoFixpoint bad: Stream :=
  match bad with
  | SCons x y => SCons x bad
  end.

"Forward One Command"で、CoFixpointを実行すると"Messages"に下記表示あり。

Recursive definition of bad is ill-formed.
In environment
bad : Stream
Invalid recursive call in the argument of "match" in
"match bad with
 | SCons x _ => SCons x bad
 end".
Recursive definition is:
"match bad with
 | SCons x _ => SCons x bad
 end".

すべての自然数に対して成り立つ

Inductive List := Nil : List | Cons : nat -> List -> List.
Fixpoint length l :=
  match l with
  | Nil => O
  | Cons n l' => S (length l') (* l' は l より "小さい" *)
  end.

CoInductive Stream := SCons : nat -> Stream -> Stream.
CoFixpoint countup (n : nat) : Stream :=
  SCons n (countup (S n)). 
(*SCons n (countup (S n)) は (countup (S n)) より大きい*)

CoInductive X : nat -> Prop :=
| X_intro : forall n, X (S n) ->X n.

Lemma X_All : forall n, X n.
Proof.
  cofix CIH. (* CIH: ∀n. X n |- ∀n. X n *)
  intro n.   (* CIH: ∀n. X n, n: nat |- X n *)
  constructor. (* CIH : ∀ n. X n, n: nat |- X (S n) *)
  apply CIH.
Qed.
Lemma X_All : forall n, X n.

"Forward One Command"すると右上窓に下記表示。

1 subgoal
______________________________________(1/1)
forall n : nat, X n
Proof.
  cofix CIH.

"Forward One Command"すると右上窓に下記表示。

1 subgoal
CIH : forall n : nat, X n
______________________________________(1/1)
forall n : nat, X n
  intro n.  

"Forward One Command"すると右上窓に下記表示。

1 subgoal
CIH : forall n : nat, X n
n : nat
______________________________________(1/1)
X n
  constructor. 

"Forward One Command"すると右上窓に下記表示。

1 subgoal
CIH : forall n : nat, X n
n : nat
______________________________________(1/1)
X (S n)
  apply CIH.

"Forward One Command"すると右上窓に下記表示。

No more subgoals.
Qed.

"Forward One Command"すると右上窓に下記表示。

X_All is defined

少しひねくれた証明

Inductive List := Nil : List | Cons : nat -> List -> List.
Fixpoint length l :=
  match l with
  | Nil => O
  | Cons n l' => S (length l') (* l' は l より "小さい" *)
  end.

CoInductive Stream := SCons : nat -> Stream -> Stream.
CoFixpoint countup (n : nat) : Stream :=
  SCons n (countup (S n)). 
(*SCons n (countup (S n)) は (countup (S n)) より大きい*)

CoInductive X : nat -> Prop :=
| X_intro : forall n, X (S n) ->X n.

Lemma X_All' : forall n, X n.
Proof.
  enough (forall n, X (S (S n)) -> X n) as H.
  - cofix CIH.
    intro n.
    apply H.
    apply CIH.
  - intros n H.
    constructor.
    constructor.
    assumption.
Qed.

変形を定理として外に出した場合

Lemma X_SSn_n : forall n, X (S (S n)) -> X n.
Proof.
  intros n H.
  constructor.
  constructor.
  assumption.
Qed.

Lemma X_All'' : forall n, X n.
Proof.
  cofix CIH.
  intro n.
  apply X_SSn_n.
  apply CIH.
Qed. 

"Forward One Command"で、最後のQed.を実行すると"Messages"に下記表示あり。


Recursive definition of CIH is ill-formed.
In environment
CIH : forall n : nat, X n
n : nat
Sub-expression "X_SSn_n n (CIH (S (S n)))" not in guarded form (should
be a constructor, an abstraction, a match, a cofix or a recursive
call).
Recursive definition is: "fun n : nat => X_SSn_n n (CIH (S (S n)))".