## Stream: Coq users

### Topic: n - 0 in dep. type?

#### Jonas Oberhauser (May 06 2021 at 09:26):

I have some cases where I have something that is convertible to `n-0` (for some variable `n : nat`) in a type, and hence not convertible to `n` (though provably equal).
I have now rolled out my own "minus" which recurses on the second argument and for which `n-0` is convertible to `n`:

``````Require Import Utf8.
Require Import Vector.

Fixpoint proj_nat {n} (i : Fin.t n) :=
match i with Fin.F1 => 1 | Fin.FS f => S (proj_nat f) end.
Fixpoint better_minus n m :=
match m with
| 0 => n
| S m' => better_minus (pred n) m'
end.

Fixpoint drop {n T} (i : Fin.t n) : t T n → t T (better_minus n (proj_nat i)) :=
match i in  Fin.t n' return t T n' → t T (better_minus n' (proj_nat i)) with
| @Fin.F1 n' => λ xs : t T (S n'), tl xs
| Fin.FS f' => λ xs, drop f' (tl xs)
end.
``````

For this specific use case it is also possible to define the desired result directly, without the projection/minus:

``````Require Import Utf8.
Require Import Vector.

Fixpoint decrease {n} (i : Fin.t n) :=
match i with
| @Fin.F1 n' => n'
| Fin.FS f' => decrease f'
end.

Fixpoint drop {n T} (i : Fin.t n) : t T n → t T (decrease i) :=
match i in  Fin.t n' return t T n' → t T (decrease i) with
| @Fin.F1 n' => λ xs : t T (S n'), tl xs
| Fin.FS f' => λ xs, drop f' (tl xs)
end.
``````

Any thoughts/suggestions?
(note that I am not rewriting with the equality proof n-0=n because I have never really gotten those kind of definitions to work smoothly in the later stages of development)

#### Jonas Oberhauser (May 06 2021 at 16:51):

I suppose another way is to redo the equality proof in the type, without using equalities :cry:

``````Fixpoint flip_O n (f : Fin.t n) :  Fin.t (n+0)
:= match f in Fin.t N return Fin.t (N+0) with
| @Fin.F1 n' => @Fin.F1 (n'+0)
| Fin.FS f => Fin.FS (flip_O _ f)
end.

Fixpoint to_nat {n} f := match f with Fin.F1 => 1 | Fin.FS f' => S (to_nat f') end.
Lemma flip_O_sanity n f : to_nat (flip_O n f) = to_nat f.
induction f ; eauto.
simpl.
now rewrite IHf.
Qed.

Fixpoint flip_S n : ∀ m, Fin.t (S (n + m)) → Fin.t (n+S m) :=
match n as Z return ∀ m, Fin.t (S (Z + m)) → Fin.t (Z+S m) with
| 0 => λ m f, f
| S n' => λ m f, Fin.caseS'  f (λ _, Fin.t (S (n'+ S m))) (@Fin.F1 (n'+S m)) (λ f', Fin.FS (flip_S n' m f'))
end.

Lemma flip_S_sanity n m f : to_nat (flip_S n m f) = to_nat f.
induction n ; eauto.
simpl.
pattern f.
apply Fin.caseS'.
- eauto.
- simpl. intros f'.
now rewrite IHn.
Qed.

Definition flip n m : Fin.t (n+m) → Fin.t (m+n).
revert m.
induction n ; eauto.
- eauto using flip_O.
- intros.
apply flip_S.
apply IHn with (m:=S m).
apply flip_S.
assumption.
Defined.

Lemma flip_sanity n m f : to_nat (flip n m f) = to_nat f.
revert m f.
induction n ; simpl ; intros.
- apply flip_O_sanity.
- rewrite flip_S_sanity.
rewrite IHn with (m:=S m).
apply flip_S_sanity.
Qed.
``````

This can't be the way to do it...

EDIT: I just stumbled across Hugo et al's comment on http://flint.cs.yale.edu/cs428/coq/doc/faq.html#htoc156 that axiom k holds on the equality in nat, with that I think just rewriting with equality should be OK :big_smile: well, that's a relief

Last updated: May 18 2024 at 10:02 UTC