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

「Coqの余帰納法でハマってしまった」
https://qiita.com/Nogikuchi/items/28f2f573537ff3e5aca5
の１行づつの実行を 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 :=
| SCons x y => SCons x bad
end.
```

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

```Recursive definition of bad is ill-formed.
In environment
Invalid recursive call in the argument of "match" in
| SCons x _ => SCons x bad
end".
Recursive definition is:
| 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)))".
```