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: Oct 13 2024 at 01:02 UTC