Unfold tactic not helpful

Using Coq
1

Hi all, I try to use the unfold tactic for fixpoint functions in proofs, but it is not really helpful

Here’s a random example (just to see the issue):

Require Import Coq.Arith.PeanoNat.
Fixpoint func (n1 n2 : nat): nat :=
  if n1 <=? n2 then 
  match n1, n2 with
    | O, O | O,_ => O
    | _, O => 1
    | S n1', S n2' => func n1' n2'
  end  
  else 
  match n1, n2 with
    | O, O | _,O => O
    | O, _ => 1
    | S n1', S n2' => func n1' n2'
  end.

Lemma testf2 : forall (n1 n2: nat), func n1 n2 = func n2 n1.
Proof.
intros.
unfold func.
destruct (n0 <=? n3) eqn:Hn.

the destruct gives an error and says: The variable n0 was not found in the current environment.

I don’t know what’s the issue with the unfold but it seems to introduce variables I cannot manipulate, ideas or solutions??

Thanks!

2

Please use code blocks like

```coq
code goes here
```

and include all necessary Require Import in your example.

1 Like
3

There are a few things to unpack here:

  • you can not destruct n0 <=? w3 because n0 and n3 are bound in the definition of the fixpoint, you can not pattern match on definition before they are introduced
  • your functions do not simplify with n0 replaced by n1 and n3 by n2 because fixpoints only reduce if they are applied to constructor of the corresponding inductive types to prevent infinite unfolding. You hence, need to destruct / do an induction on n1 and n2 to simplify your definitions. I don’t like this definitions so it might not be the prettiest but here a proof
Lemma testf2 : forall (n1 n2: nat), func n1 n2 = func n2 n1.
Definition leb_total n m : n <? m = true \/ n = m \/ m <? n = true.
Admitted.

Definition ltb_leb n m : n <? m = true -> n <=? m = true.
Admitted.

Lemma testf2 : forall (n1 n2: nat), func n1 n2 = func n2 n1.
Proof.
  intros n1. induction n1; intros n2; destruct n2; cbn.
  1-3: reflexivity.
  destruct (leb_total n1 n2) as [H | [H | H]].
  - rewrite (ltb_leb _ _ H). rewrite Nat.leb_antisym, H. cbn. apply IHn1.
  - rewrite <- H. rewrite Nat.leb_refl. apply IHn1.
  - rewrite (ltb_leb _ _ H). rewrite Nat.leb_antisym, H. cbn. apply IHn1.
Qed.
1 Like