The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Jesper,

  you could alternatively use the [depelim] tactic that's part

of Equations which would avoid the use of an axiom in this case 

(as the index type is discriminable as fin_case above shows as well).

Either way using induction/case analysis on the vector or index first.

From Equations Require Import Equations DepElimDec.

Lemma replace_fact1 {A n} (xs : Vector.t A n) i x : (Vector.replace xs i x)[@i] = x.

Proof.

  induction xs.

  - depelim i.

  - depelim i.

    + reflexivity.

    + now cbn.

Qed.

Lemma replace_fact1' {A n} (xs : Vector.t A n) i x : (Vector.replace xs i x)[@i] = x.

Proof.

  induction i.

  - depelim xs. simpl. reflexivity.

  - depelim xs. simpl. auto.

Qed.

Print Assumptions replace_fact1.

Print Assumptions replace_fact1'.

Best,

-- Matthieu

On Sun, Dec 17, 2017 at 2:42 PM Adam Chlipala <adamc AT csail.mit.edu> wrote:

I went about the proof in the other direction (induction on vector, case analysis on index).  My intention was for this sort of thing to be covered well in CPDT (maybe in the section about how to avoid axioms), so I'll appreciate any suggestions on how I might have missed the requisite ideas.

Lemma fin_case : forall {n} (i : Fin.t n),
    match n return Fin.t n -> Prop with
    | O => fun _ => False
    | S _ => fun i => i = Fin.F1 \/ exists i', i = Fin.FS i'
    end i.
Proof.
  destruct i; eauto.
Qed.

Lemma replace_fact1 : forall A n (xs : Vector.t A n) i x, (Vector.replace xs i x)[@i] = x.
Proof.
  induction xs; intro i; destruct (fin_case i); firstorder (subst; simpl); eauto.
Qed.

On 12/17/2017 07:37 AM, Jasper Hugunin wrote:

Hello Matěj,

The reason you are missing the induction hypothesis is you never performed an induction (or a fixpoint).

You can get the induction hypothesis by starting off with something like

  refine ((fix inner n (i : Fin.t n) (xs : Vector.t A n) := match i as i' in Fin.t n' ...) n i xs)

However, when I tried that route, I got stuck at Qed with a message saying

the induction hypothesis was not used on a smaller term.

Here is a way to prove that lemma without axioms in pure Gallina:

Fixpoint replace_fact1 {A n} (xs : Vector.t A n) i x

  : (Vector.replace xs i x)[@i] = x

  := match i in Fin.t n'

     return forall (xs : Vector.t A n'), (Vector.replace xs i x)[@i] = x

     with

     | Fin.F1 => fun xs => Vector.caseS' xs

       (fun xs => (Vector.replace xs Fin.F1 x)[@Fin.F1] = x)

       (fun a xs' => eq_refl : x = x)

     | Fin.FS i' => fun xs => Vector.caseS' xs

       (fun xs => (Vector.replace xs (Fin.FS i') x)[@Fin.FS i'] = x)

       (fun a xs' => replace_fact1 xs' i' x

        : (Vector.replace xs' i' x)[@i'] = x)

     end xs.

I don't use Ltac, so I can't help translating the above into tactics,

but hopefully the above is useful in understanding what is going on behind the scenes.

Perhaps just writing the outer fix+match (the fix is embedded in the Fixpoint command)

as your refine would be enough to get started.

- Jasper Hugunin

On Sun, Dec 17, 2017 at 8:34 PM, Matěj Grabovský <matej.grabovsky AT gmail.com> wrote:

Hello.

I'm trying to prove the following, apparently simple statement about
the Vector.replace function from the standard library (the full code
is at http://lpaste.net/360859):

    forall {A n} (xs : Vector.t A n) i x, (Vector.replace xs i x)[@i] = x

Although I can prove this just fine using Program, I'd also like to
perform the proof without it, without assuming additional axioms.
However, I can't quite wrap my head around what's going on with all
the type dependencies.

I can destruct the with an intricate matching trick, but I'm unable to
proceed in the latter branch as I need more information for the proof
to progress.

What is the Coq canonical/recommended approach to dependent induction
without on inductives indexed by types with decidable equality? Is
there a general approach to this? If not, how would I go about this in
the Vector case?

Note that I'm not looking for alternatives to stdlib Vector or
specialised libraries as of now. I'd very much like to understand the
concept in vanilla Coq first.

Best regards,

Matěj