n - 0 in dep. type? · Coq users · Zulip Chat Archive

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.

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

Stream: Coq users

Topic: n - 0 in dep. type?

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

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