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)

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: Jan 29 2023 at 03:28 UTC