I have the following code:

```
From HoTT Require Import HoTT.
Local Open Scope path_scope.
Local Open Scope equiv_scope.
Local Open Scope fibration_scope.
Local Open Scope nat_scope.
Fixpoint nat_iter (C : Type) (c0 : C) (csuc : C -> C) (n : nat) : C :=
match n with
| 0 => c0
| S n => csuc (nat_iter C c0 csuc n)
end.
Definition sigsuc (P : nat -> Type) (psuc : forall n, P n -> P (S n)) (p : {n | P n}) : {n | P n} :=
match p with
| (n ; pn) => (S n; psuc _ pn)
end.
Definition nat_rec' (P : nat -> Type) (p0 : P 0) (psuc : forall n, P n -> P (S n)) (n : nat) : {n | P n} :=
nat_iter (sig P) (0 ; p0) (sigsuc P psuc) n.
Lemma nat_rec_proj1 : forall (P : nat -> Type) (p0 : P 0) (psuc : forall n, P n -> P (S n)) (n : nat), (nat_iter (sig P) (0 ; p0) (sigsuc P psuc) n) .1 = n.
Proof.
intros P p0 psuc n. induction n as [| n' IH].
- reflexivity.
- unfold nat_iter. simpl. apply eq_S. fold (nat_iter {n | P n} (0; p0) (sigsuc P psuc) n').
```

When I try to apply fold at the end my context looks like:

```
((fix nat_iter (C : Type) (c0 : C) (csuc : C -> C) (n : nat) {struct n} : C :=
match n with
| 0 => c0
| n0.+1 => csuc (nat_iter C c0 csuc n0)
end) {x : _ & P x} (0; p0) (sigsuc P psuc) n').1 = n'
```

However, the fold tactic doesn't seem to do anything, is there something I am doing wrong here or some obvious mistake I am making?

I don't get `fold`

either but it might be better to not `unfold nat_iter`

in the first place.

do you have a suggestion for alternatives? the reason I am doing it is so I can use the inductive hypothesis but there might be some better way to perform a small amount of computation here

Trying using change

Looks like `cbn`

might be the move

This works:

```
Lemma nat_rec_proj1 : forall (P : nat -> Type) (p0 : P 0) (psuc : forall n, P n -> P (S n)) (n : nat), (nat_iter (sig P) (0 ; p0) (sigsuc P psuc) n) .1 = n.
Proof.
intros P p0 psuc n. induction n as [| n' IH].
- reflexivity.
- cbn. rewrite -> IH. reflexivity.
Qed.
```

Thanks @Li-yao for the prompt!

`change`

allows you to turn the goal into a shape you know is definitionally the same

even with `simpl`

, it's surprisingly you'd need `unfold nat_iter`

...

does `- simpl. rewrite -> IH. reflexivity.`

not give the same result?

Oh, it does! I thought I'd tried that first but I think it was late and I misread how the goal changed. Thanks!

Last updated: Jun 16 2024 at 01:42 UTC