## Stream: Coq users

### Topic: Struggling with fold in proof

#### Callan McGill (Jan 27 2022 at 19:26):

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?

#### Li-yao (Jan 27 2022 at 19:45):

I don't get `fold` either but it might be better to not `unfold nat_iter` in the first place.

#### Callan McGill (Jan 27 2022 at 19:57):

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

#### Ali Caglayan (Jan 27 2022 at 19:59):

Trying using change

#### Callan McGill (Jan 27 2022 at 19:59):

Looks like `cbn` might be the move

#### Callan McGill (Jan 27 2022 at 19:59):

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!

#### Ali Caglayan (Jan 27 2022 at 19:59):

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

#### Paolo Giarrusso (Jan 27 2022 at 21:28):

even with `simpl`, it's surprisingly you'd need `unfold nat_iter`...

#### Paolo Giarrusso (Jan 27 2022 at 21:29):

does `- simpl. rewrite -> IH. reflexivity.` not give the same result?

#### Callan McGill (Jan 27 2022 at 21:53):

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