Stream: Coq users

Topic: Struggling with fold in proof


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Ali Caglayan (Jan 27 2022 at 19:59):

Trying using change

view this post on Zulip Callan McGill (Jan 27 2022 at 19:59):

Looks like cbn might be the move

view this post on Zulip 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!

view this post on Zulip Ali Caglayan (Jan 27 2022 at 19:59):

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

view this post on Zulip Paolo Giarrusso (Jan 27 2022 at 21:28):

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

view this post on Zulip Paolo Giarrusso (Jan 27 2022 at 21:29):

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

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC