The Coq mailing list

[Matěj Grabovský <matej.grabovsky AT gmail.com>]

Thank you all for your helpful comments. I believe I now have a
slightly better insight into this pattern in Coq.

I really like Adam's idea. I am aware of CPDT, though I hadn't looked
at that specific chapter. It does seem useful at the moment.

On 17 December 2017 at 20:05, Matthieu Sozeau 
<mattam AT mattam.org>
 wrote:
> 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
>>
>>
>>
>