diff options
Diffstat (limited to 'docs/proof/Array.html')
| -rw-r--r-- | docs/proof/Array.html | 547 |
1 files changed, 547 insertions, 0 deletions
diff --git a/docs/proof/Array.html b/docs/proof/Array.html new file mode 100644 index 0000000..703b68b --- /dev/null +++ b/docs/proof/Array.html @@ -0,0 +1,547 @@ +<?xml version="1.0" encoding="utf-8" ?> +<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"> +<html xmlns="http://www.w3.org/1999/xhtml" class="alectryon-standalone" xml:lang="en" lang="en"> +<head> +<meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> +<meta name="generator" content="Docutils 0.16: http://docutils.sourceforge.net/" /> +<title>Array.v</title> +<link rel="stylesheet" href="alectryon.css" type="text/css" /> +<link rel="stylesheet" href="docutils_basic.css" type="text/css" /> +<link rel="stylesheet" href="tango_subtle.css" type="text/css" /> +<link rel="stylesheet" href="tango_subtle.min.css" type="text/css" /> +<script type="text/javascript" src="alectryon.js"></script> +<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/IBM-type/0.5.4/css/ibm-type.min.css" integrity="sha512-sky5cf9Ts6FY1kstGOBHSybfKqdHR41M0Ldb0BjNiv3ifltoQIsg0zIaQ+wwdwgQ0w9vKFW7Js50lxH9vqNSSw==" crossorigin="anonymous" /> +<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/firacode/5.2.0/fira_code.min.css" integrity="sha512-MbysAYimH1hH2xYzkkMHB6MqxBqfP0megxsCLknbYqHVwXTCg9IqHbk+ZP/vnhO8UEW6PaXAkKe2vQ+SWACxxA==" crossorigin="anonymous" /> +</head> +<body> +<div class="alectryon-root alectryon-floating"><div class="document"> + + +<pre class="alectryon-io"><!-- Generator: Alectryon v1.0 --><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Set Implicit Arguments</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Require Import</span> Lia.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Require Import</span> Vericertlib.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">From</span> Coq <span class="kn">Require Import</span> Lists.List Datatypes.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Import</span> ListNotations.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Local Open Scope</span> nat_scope.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Record</span> <span class="nf">Array</span> (<span class="nv">A</span> : <span class="kt">Type</span>) : <span class="kt">Type</span> := + mk_array + { arr_contents : list A + ; arr_length : nat + ; arr_wf : length arr_contents = arr_length + }.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">make_array</span> {<span class="nv">A</span> : <span class="kt">Type</span>} (<span class="nv">l</span> : list A) : Array A := + @mk_array A l (length l) eq_refl.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Fixpoint</span> <span class="nf">list_set</span> {<span class="nv">A</span> : <span class="kt">Type</span>} (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A) (<span class="nv">l</span> : list A) {<span class="nv">struct</span> <span class="nv">l</span>} : list A := + <span class="kr">match</span> i, l <span class="kr">with</span> + | _, nil => nil + | S n, h :: t => h :: list_set n x t + | O, h :: t => x :: t + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk0" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk0"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_set_spec1</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> <span class="nv">l</span> <span class="nv">i</span> (<span class="nv">x</span> : A), + i < length l -> nth_error (list_set i x l) i = Some x.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">l</span> : list A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +i < length l -> nth_error (list_set i x l) i = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk1" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk1"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">l</span> : list A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +i < length l -> nth_error (list_set i x l) i = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk2" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk2"><span class="highlight"><span class="nb">induction</span> l; <span class="nb">intros</span>; <span class="nb">destruct</span> i; crush; <span class="nb">firstorder</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHl</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +i < length l -> nth_error (list_set i x l) i = Some x</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">S i < S (length l)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (list_set i x l) i = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">intuition</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Resolve</span> list_set_spec1 : array.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk3" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk3"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_set_spec2</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> <span class="nv">l</span> <span class="nv">i</span> (<span class="nv">x</span> : A) <span class="nv">d</span>, + i < length l -> nth i (list_set i x l) d = x.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">l</span> : list A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> <span class="nv">d</span> : A), +i < length l -> nth i (list_set i x l) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk4" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk4"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">l</span> : list A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> <span class="nv">d</span> : A), +i < length l -> nth i (list_set i x l) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk5" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk5"><span class="highlight"><span class="nb">induction</span> l; <span class="nb">intros</span>; <span class="nb">destruct</span> i; crush; <span class="nb">firstorder</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHl</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> (<span class="nv">i</span> : nat) (<span class="nv">x</span> <span class="nv">d</span> : A), i < length l -> nth i (list_set i x l) d = x</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x, d</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">S i < S (length l)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth i (list_set i x l) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">intuition</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Resolve</span> list_set_spec2 : array.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk6" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk6"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_set_spec3</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> <span class="nv">l</span> <span class="nv">i1</span> <span class="nv">i2</span> (<span class="nv">x</span> : A), + i1 <> i2 -> + nth_error (list_set i1 x l) i2 = nth_error l i2.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">l</span> : list A) (<span class="nv">i1</span> <span class="nv">i2</span> : nat) (<span class="nv">x</span> : A), +i1 <> i2 -> +nth_error (list_set i1 x l) i2 = nth_error l i2</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk7" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk7"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">l</span> : list A) (<span class="nv">i1</span> <span class="nv">i2</span> : nat) (<span class="nv">x</span> : A), +i1 <> i2 -> +nth_error (list_set i1 x l) i2 = nth_error l i2</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">induction</span> l; <span class="nb">intros</span>; <span class="nb">destruct</span> i1; <span class="nb">destruct</span> i2; crush; <span class="nb">firstorder</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Resolve</span> list_set_spec3 : array.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk8" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk8"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">array_set_wf</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> <span class="nv">l</span> <span class="nv">ln</span> <span class="nv">i</span> (<span class="nv">x</span> : A), + length l = ln -> length (list_set i x l) = ln.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">l</span> : list A) (<span class="nv">ln</span> <span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +length l = ln -> length (list_set i x l) = ln</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk9" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk9"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">l</span> : list A) (<span class="nv">ln</span> <span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +length l = ln -> length (list_set i x l) = ln</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chka" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chka"><span class="highlight"><span class="nb">induction</span> l; <span class="nb">intros</span>; <span class="nb">destruct</span> i; <span class="nb">auto</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHl</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> (<span class="nv">ln</span> <span class="nv">i</span> : nat) (<span class="nv">x</span> : A), length l = ln -> length (list_set i x l) = ln</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">ln, i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">length (a :: l) = ln</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length (list_set (S i) x (a :: l)) = ln</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight">invert H; crush; <span class="nb">auto</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">array_set</span> {<span class="nv">A</span> : <span class="kt">Type</span>} (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A) (<span class="nv">a</span> : Array A) := + <span class="kr">let</span> <span class="nv">l</span> := a.(arr_contents) <span class="kr">in</span> + <span class="kr">let</span> <span class="nv">ln</span> := a.(arr_length) <span class="kr">in</span> + <span class="kr">let</span> <span class="nv">WF</span> := a.(arr_wf) <span class="kr">in</span> + @mk_array A (list_set i x l) ln (@array_set_wf A l ln i x WF).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chkb" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chkb"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">array_set_spec1</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> <span class="nv">a</span> <span class="nv">i</span> (<span class="nv">x</span> : A), + i < a.(arr_length) -> nth_error ((array_set i x a).(arr_contents)) i = Some x.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +i < arr_length a -> +nth_error (arr_contents (array_set i x a)) i = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chkc" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chkc"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +i < arr_length a -> +nth_error (arr_contents (array_set i x a)) i = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chkd" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chkd"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < arr_length a</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (arr_contents (array_set i x a)) i = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chke" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chke"><span class="highlight"><span class="nb">rewrite</span> <- a.(arr_wf) <span class="kr">in</span> H.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (arr_contents (array_set i x a)) i = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chkf" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chkf"><span class="highlight"><span class="nb">unfold</span> array_set.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error + (arr_contents + {| + arr_contents := list_set i x (arr_contents a); + arr_length := arr_length a; + arr_wf := array_set_wf (arr_contents a) i x + (arr_wf a) |}) i = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk10" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk10"><span class="highlight">crush.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (list_set i x (arr_contents a)) i = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">eauto with</span> array.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Resolve</span> array_set_spec1 : array.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk11" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk11"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">array_set_spec2</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> <span class="nv">a</span> <span class="nv">i</span> (<span class="nv">x</span> : A) <span class="nv">d</span>, + i < a.(arr_length) -> nth i ((array_set i x a).(arr_contents)) d = x.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> <span class="nv">d</span> : A), +i < arr_length a -> +nth i (arr_contents (array_set i x a)) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk12" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk12"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> <span class="nv">d</span> : A), +i < arr_length a -> +nth i (arr_contents (array_set i x a)) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk13" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk13"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x, d</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < arr_length a</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth i (arr_contents (array_set i x a)) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk14" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk14"><span class="highlight"><span class="nb">rewrite</span> <- a.(arr_wf) <span class="kr">in</span> H.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x, d</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth i (arr_contents (array_set i x a)) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk15" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk15"><span class="highlight"><span class="nb">unfold</span> array_set.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x, d</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth i + (arr_contents + {| + arr_contents := list_set i x (arr_contents a); + arr_length := arr_length a; + arr_wf := array_set_wf (arr_contents a) i x + (arr_wf a) |}) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk16" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk16"><span class="highlight">crush.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x, d</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth i (list_set i x (arr_contents a)) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">eauto with</span> array.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Hint Resolve</span> array_set_spec2 : array.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk17" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk17"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">array_set_len</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> <span class="nv">a</span> <span class="nv">i</span> (<span class="nv">x</span> : A), + a.(arr_length) = (array_set i x a).(arr_length).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +arr_length a = arr_length (array_set i x a)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk18" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk18"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +arr_length a = arr_length (array_set i x a)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk19" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk19"><span class="highlight"><span class="nb">unfold</span> array_set.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +arr_length a = +arr_length + {| + arr_contents := list_set i x (arr_contents a); + arr_length := arr_length a; + arr_wf := array_set_wf (arr_contents a) i x + (arr_wf a) |}</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight">crush.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">array_get_error</span> {<span class="nv">A</span> : <span class="kt">Type</span>} (<span class="nv">i</span> : nat) (<span class="nv">a</span> : Array A) : option A := + nth_error a.(arr_contents) i.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk1a" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk1a"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">array_get_error_equal</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> (<span class="nv">a</span> <span class="nv">b</span> : Array A) <span class="nv">i</span>, + a.(arr_contents) = b.(arr_contents) -> + array_get_error i a = array_get_error i b.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> <span class="nv">b</span> : Array A) (<span class="nv">i</span> : nat), +arr_contents a = arr_contents b -> +array_get_error i a = array_get_error i b</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk1b" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk1b"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> <span class="nv">b</span> : Array A) (<span class="nv">i</span> : nat), +arr_contents a = arr_contents b -> +array_get_error i a = array_get_error i b</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk1c" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk1c"><span class="highlight"><span class="nb">unfold</span> array_get_error.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> <span class="nv">b</span> : Array A) (<span class="nv">i</span> : nat), +arr_contents a = arr_contents b -> +nth_error (arr_contents a) i = +nth_error (arr_contents b) i</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight">crush.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk1d" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk1d"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">array_get_error_bound</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> (<span class="nv">a</span> : Array A) <span class="nv">i</span>, + i < a.(arr_length) -> <span class="kr">exists</span> <span class="nv">x</span>, array_get_error i a = Some x.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat), +i < arr_length a -> +<span class="kr">exists</span> <span class="nv">x</span> : A, array_get_error i a = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk1e" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk1e"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat), +i < arr_length a -> +<span class="kr">exists</span> <span class="nv">x</span> : A, array_get_error i a = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk1f" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk1f"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < arr_length a</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">exists</span> <span class="nv">x</span> : A, array_get_error i a = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk20" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk20"><span class="highlight"><span class="nb">rewrite</span> <- a.(arr_wf) <span class="kr">in</span> H.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">exists</span> <span class="nv">x</span> : A, array_get_error i a = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk21" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk21"><span class="highlight"><span class="nb">assert</span> (~ length (arr_contents a) <= i) <span class="bp">by</span> <span class="bp">lia</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">~ length (arr_contents a) <= i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">exists</span> <span class="nv">x</span> : A, array_get_error i a = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk22" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk22"><span class="highlight"><span class="nb">pose proof</span> (nth_error_None a.(arr_contents) i).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">~ length (arr_contents a) <= i</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nth_error (arr_contents a) i = None <-> +length (arr_contents a) <= i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">exists</span> <span class="nv">x</span> : A, array_get_error i a = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk23" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk23"><span class="highlight"><span class="nb">apply</span> not_iff_compat <span class="kr">in</span> H1.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">~ length (arr_contents a) <= i</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nth_error (arr_contents a) i <> None <-> +~ length (arr_contents a) <= i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">exists</span> <span class="nv">x</span> : A, array_get_error i a = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk24" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk24"><span class="highlight"><span class="nb">apply</span> <- H1 <span class="kr">in</span> H0.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < length (arr_contents a)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nth_error (arr_contents a) i <> None</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nth_error (arr_contents a) i <> None <-> +~ length (arr_contents a) <= i</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">exists</span> <span class="nv">x</span> : A, array_get_error i a = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">destruct</span> (nth_error (arr_contents a) i) <span class="nb">eqn</span>:EQ; <span class="kp">try</span> <span class="bp">contradiction</span>; <span class="nb">eauto</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk25" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk25"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">array_get_error_set_bound</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> (<span class="nv">a</span> : Array A) <span class="nv">i</span> <span class="nv">x</span>, + i < a.(arr_length) -> array_get_error i (array_set i x a) = Some x.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +i < arr_length a -> +array_get_error i (array_set i x a) = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk26" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk26"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A), +i < arr_length a -> +array_get_error i (array_set i x a) = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk27" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk27"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < arr_length a</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">array_get_error i (array_set i x a) = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk28" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk28"><span class="highlight"><span class="nb">unfold</span> array_get_error.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < arr_length a</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (arr_contents (array_set i x a)) i = Some x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">eauto with</span> array.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk29" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk29"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">array_gso</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> (<span class="nv">a</span> : Array A) <span class="nv">i1</span> <span class="nv">i2</span> <span class="nv">x</span>, + i1 <> i2 -> + array_get_error i2 (array_set i1 x a) = array_get_error i2 a.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i1</span> <span class="nv">i2</span> : nat) (<span class="nv">x</span> : A), +i1 <> i2 -> +array_get_error i2 (array_set i1 x a) = +array_get_error i2 a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk2a" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk2a"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i1</span> <span class="nv">i2</span> : nat) (<span class="nv">x</span> : A), +i1 <> i2 -> +array_get_error i2 (array_set i1 x a) = +array_get_error i2 a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk2b" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk2b"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i1, i2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i1 <> i2</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">array_get_error i2 (array_set i1 x a) = +array_get_error i2 a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk2c" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk2c"><span class="highlight"><span class="nb">unfold</span> array_get_error.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i1, i2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i1 <> i2</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (arr_contents (array_set i1 x a)) i2 = +nth_error (arr_contents a) i2</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk2d" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk2d"><span class="highlight"><span class="nb">unfold</span> array_set.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i1, i2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i1 <> i2</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error + (arr_contents + {| + arr_contents := list_set i1 x (arr_contents a); + arr_length := arr_length a; + arr_wf := array_set_wf (arr_contents a) i1 x + (arr_wf a) |}) i2 = +nth_error (arr_contents a) i2</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk2e" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk2e"><span class="highlight">crush.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i1, i2</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i1 <> i2</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (list_set i1 x (arr_contents a)) i2 = +nth_error (arr_contents a) i2</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">eauto with</span> array.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">array_get</span> {<span class="nv">A</span> : <span class="kt">Type</span>} (<span class="nv">i</span> : nat) (<span class="nv">x</span> : A) (<span class="nv">a</span> : Array A) : A := + nth i a.(arr_contents) x.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk2f" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk2f"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">array_get_set_bound</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> (<span class="nv">a</span> : Array A) <span class="nv">i</span> <span class="nv">x</span> <span class="nv">d</span>, + i < a.(arr_length) -> array_get i d (array_set i x a) = x.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> <span class="nv">d</span> : A), +i < arr_length a -> +array_get i d (array_set i x a) = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk30" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk30"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> <span class="nv">d</span> : A), +i < arr_length a -> +array_get i d (array_set i x a) = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk31" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk31"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x, d</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < arr_length a</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">array_get i d (array_set i x a) = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk32" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk32"><span class="highlight"><span class="nb">unfold</span> array_get.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x, d</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < arr_length a</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth i (arr_contents (array_set i x a)) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">eauto with</span> array.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk33" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk33"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">array_get_get_error</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> (<span class="nv">a</span> : Array A) <span class="nv">i</span> <span class="nv">x</span> <span class="nv">d</span>, + array_get_error i a = Some x -> + array_get i d a = x.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> <span class="nv">d</span> : A), +array_get_error i a = Some x -> array_get i d a = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk34" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk34"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : Array A) (<span class="nv">i</span> : nat) (<span class="nv">x</span> <span class="nv">d</span> : A), +array_get_error i a = Some x -> array_get i d a = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk35" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk35"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x, d</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">array_get_error i a = Some x</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">array_get i d a = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk36" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk36"><span class="highlight"><span class="nb">unfold</span> array_get.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x, d</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">array_get_error i a = Some x</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth i (arr_contents a) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk37" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk37"><span class="highlight"><span class="nb">unfold</span> array_get_error <span class="kr">in</span> H.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x, d</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nth_error (arr_contents a) i = Some x</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth i (arr_contents a) d = x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">auto using</span> nth_error_nth.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +<span class="sd">(** Tail recursive version of standard library function. *)</span> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Fixpoint</span> <span class="nf">list_repeat'</span> {<span class="nv">A</span> : <span class="kt">Type</span>} (<span class="nv">acc</span> : list A) (<span class="nv">a</span> : A) (<span class="nv">n</span> : nat) : list A := + <span class="kr">match</span> n <span class="kr">with</span> + | O => acc + | S n => list_repeat' (a::acc) a n + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk38" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk38"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_repeat'_len</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : <span class="kr">forall</span> (<span class="nv">a</span> : A) <span class="nv">n</span> <span class="nv">l</span>, + length (list_repeat' l a n) = (n + Datatypes.length l)%nat.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : A) (<span class="nv">n</span> : nat) (<span class="nv">l</span> : list A), +length (list_repeat' l a n) = n + length l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk39" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk39"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : A) (<span class="nv">n</span> : nat) (<span class="nv">l</span> : list A), +length (list_repeat' l a n) = n + length l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk3a" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk3a"><span class="highlight"><span class="nb">induction</span> n; <span class="nb">intros</span>; crush; <span class="kp">try</span> <span class="bp">reflexivity</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">l</span> : list A, length (list_repeat' l a n) = n + length l</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length (list_repeat' (a :: l) a n) = S (n + length l)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk3b" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk3b"><span class="highlight"><span class="nb">specialize</span> (IHn (a :: l)).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">length (list_repeat' (a :: l) a n) = n + length (a :: l)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length (list_repeat' (a :: l) a n) = S (n + length l)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk3c" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk3c"><span class="highlight"><span class="nb">rewrite</span> IHn.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">length (list_repeat' (a :: l) a n) = n + length (a :: l)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">n + length (a :: l) = S (n + length l)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight">crush.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk3d" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk3d"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_repeat'_app</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : <span class="kr">forall</span> (<span class="nv">a</span> : A) <span class="nv">n</span> <span class="nv">l</span>, + list_repeat' l a n = list_repeat' [] a n ++ l.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : A) (<span class="nv">n</span> : nat) (<span class="nv">l</span> : list A), +list_repeat' l a n = list_repeat' [] a n ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk3e" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk3e"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : A) (<span class="nv">n</span> : nat) (<span class="nv">l</span> : list A), +list_repeat' l a n = list_repeat' [] a n ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk3f" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk3f"><span class="highlight"><span class="nb">induction</span> n; <span class="nb">intros</span>; crush; <span class="kp">try</span> <span class="bp">reflexivity</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">l</span> : list A, list_repeat' l a n = list_repeat' [] a n ++ l</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' (a :: l) a n = list_repeat' [a] a n ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk40" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk40"><span class="highlight"><span class="nb">pose proof</span> IHn.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">l</span> : list A, list_repeat' l a n = list_repeat' [] a n ++ l</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">l</span> : list A, +list_repeat' l a n = list_repeat' [] a n ++ l</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' (a :: l) a n = list_repeat' [a] a n ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk41" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk41"><span class="highlight"><span class="nb">specialize</span> (H (a :: l)).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">l</span> : list A, list_repeat' l a n = list_repeat' [] a n ++ l</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list_repeat' (a :: l) a n = +list_repeat' [] a n ++ a :: l</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' (a :: l) a n = list_repeat' [a] a n ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk42" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk42"><span class="highlight"><span class="nb">rewrite</span> H.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">l</span> : list A, list_repeat' l a n = list_repeat' [] a n ++ l</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list_repeat' (a :: l) a n = +list_repeat' [] a n ++ a :: l</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ a :: l = +list_repeat' [a] a n ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk43" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk43"><span class="highlight"><span class="nb">clear</span> H.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">l</span> : list A, list_repeat' l a n = list_repeat' [] a n ++ l</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ a :: l = +list_repeat' [a] a n ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk44" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk44"><span class="highlight"><span class="nb">specialize</span> (IHn (a :: nil)).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list_repeat' [a] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ a :: l = +list_repeat' [a] a n ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk45" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk45"><span class="highlight"><span class="nb">rewrite</span> IHn.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list_repeat' [a] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ a :: l = +(list_repeat' [] a n ++ [a]) ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk46" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk46"><span class="highlight"><span class="nb">clear</span> IHn.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ a :: l = +(list_repeat' [] a n ++ [a]) ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk47" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk47"><span class="highlight"><span class="nb">remember</span> (list_repeat' [] a n) <span class="kr">as</span> l0.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l, l0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">Heql0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">l0 = list_repeat' [] a n</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">l0 ++ a :: l = (l0 ++ [a]) ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk48" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk48"><span class="highlight"><span class="nb">rewrite</span> <- app_assoc.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l, l0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">Heql0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">l0 = list_repeat' [] a n</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">l0 ++ a :: l = l0 ++ [a] ++ l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">f_equal</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk49" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk49"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_repeat'_head_tail</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : <span class="kr">forall</span> <span class="nv">n</span> (<span class="nv">a</span> : A), + a :: list_repeat' [] a n = list_repeat' [] a n ++ [a].</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), +a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk4a" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk4a"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), +a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk4b" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk4b"><span class="highlight"><span class="nb">induction</span> n; <span class="nb">intros</span>; crush; <span class="kp">try</span> <span class="bp">reflexivity</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a :: list_repeat' [a] a n = +list_repeat' [a] a n ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk4c" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk4c"><span class="highlight"><span class="nb">rewrite</span> list_repeat'_app.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a :: list_repeat' [] a n ++ [a] = +(list_repeat' [] a n ++ [a]) ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk4d" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk4d"><span class="highlight"><span class="nb">replace</span> (a :: list_repeat' [] a n ++ [a]) <span class="kr">with</span> (list_repeat' [] a n ++ [a] ++ [a]).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ [a] ++ [a] = +(list_repeat' [] a n ++ [a]) ++ [a]</span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="array-v-chk4e" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="array-v-chk4e"><hr></label><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ [a] ++ [a] = +a :: list_repeat' [] a n ++ [a]</span></div></blockquote></div></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk4f" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk4f"><span class="highlight"><span class="mi">2</span>: {</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ [a] ++ [a] = +a :: list_repeat' [] a n ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk50" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk50"><span class="highlight"><span class="nb">rewrite</span> app_comm_cons.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ [a] ++ [a] = +(a :: list_repeat' [] a n) ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk51" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk51"><span class="highlight"><span class="nb">rewrite</span> IHn; <span class="nb">auto</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ [a] ++ [a] = +(list_repeat' [] a n ++ [a]) ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk52" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk52"><span class="highlight"><span class="nb">rewrite</span> app_assoc.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">(list_repeat' [] a n ++ [a]) ++ [a] = +(list_repeat' [] a n ++ [a]) ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="bp">reflexivity</span>.</span></span><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk53" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk53"><span class="highlight">}</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a n ++ [a] ++ [a] = +(list_repeat' [] a n ++ [a]) ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk54" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk54"><span class="highlight"><span class="nb">rewrite</span> app_assoc.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> : A, a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">(list_repeat' [] a n ++ [a]) ++ [a] = +(list_repeat' [] a n ++ [a]) ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="bp">reflexivity</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk55" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk55"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_repeat'_cons</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : <span class="kr">forall</span> (<span class="nv">a</span> : A) <span class="nv">n</span>, + list_repeat' [a] a n = a :: list_repeat' [] a n.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : A) (<span class="nv">n</span> : nat), +list_repeat' [a] a n = a :: list_repeat' [] a n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk56" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk56"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">a</span> : A) (<span class="nv">n</span> : nat), +list_repeat' [a] a n = a :: list_repeat' [] a n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk57" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk57"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [a] a n = a :: list_repeat' [] a n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk58" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk58"><span class="highlight"><span class="nb">rewrite</span> list_repeat'_head_tail; <span class="nb">auto</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [a] a n = list_repeat' [] a n ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">apply</span> list_repeat'_app.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">list_repeat</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : A -> nat -> list A := list_repeat' nil.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk59" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk59"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_repeat_len</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : <span class="kr">forall</span> <span class="nv">n</span> (<span class="nv">a</span> : A), length (list_repeat a n) = n.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), length (list_repeat a n) = n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk5a" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk5a"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), length (list_repeat a n) = n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk5b" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk5b"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length (list_repeat a n) = n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk5c" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk5c"><span class="highlight"><span class="nb">unfold</span> list_repeat.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length (list_repeat' [] a n) = n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk5d" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk5d"><span class="highlight"><span class="nb">rewrite</span> list_repeat'_len.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">n + length [] = n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight">crush.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk5e" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk5e"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">dec_list_repeat_spec</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : <span class="kr">forall</span> <span class="nv">n</span> (<span class="nv">a</span> : A) <span class="nv">a'</span>, + (<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {~ x' = x}) -> + In a' (list_repeat a n) -> a' = a.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> <span class="nv">a'</span> : A), +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat a n) -> a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk5f" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk5f"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> <span class="nv">a'</span> : A), +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat a n) -> a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk60" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk60"><span class="highlight"><span class="nb">induction</span> n; <span class="nb">intros</span>; crush.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> In a' (list_repeat a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' (list_repeat a (S n))</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk61" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk61"><span class="highlight"><span class="nb">unfold</span> list_repeat <span class="kr">in</span> *.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' (list_repeat' [] a (S n))</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk62" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk62"><span class="highlight">crush.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' (list_repeat' [a] a n)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk63" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk63"><span class="highlight"><span class="nb">rewrite</span> list_repeat'_app <span class="kr">in</span> H.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' (list_repeat' [] a n ++ [a])</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk64" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk64"><span class="highlight"><span class="nb">pose proof</span> (X a a').</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' (list_repeat' [] a n ++ [a])</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">{a' = a} + {a' <> a}</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk65" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk65"><span class="highlight"><span class="nb">destruct</span> H0; <span class="nb">auto</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' (list_repeat' [] a n ++ [a])</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">a' <> a</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> + <span class="c">(* This is actually a degenerate case, not an unprovable goal. *)</span> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk66" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk66"><span class="highlight"><span class="nb">pose proof</span> (in_app_or (list_repeat' [] a n) ([a])).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' (list_repeat' [] a n ++ [a])</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">a' <> a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a0</span> : A, +In a0 (list_repeat' [] a n ++ [a]) -> +In a0 (list_repeat' [] a n) \/ In a0 [a]</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk67" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk67"><span class="highlight"><span class="nb">apply</span> H0 <span class="kr">in</span> H.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' (list_repeat' [] a n) \/ In a' [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">a' <> a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a0</span> : A, +In a0 (list_repeat' [] a n ++ [a]) -> +In a0 (list_repeat' [] a n) \/ In a0 [a]</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk68" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk68"><span class="highlight">invert H.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">a' <> a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a0</span> : A, +In a0 (list_repeat' [] a n ++ [a]) -> +In a0 (list_repeat' [] a n) \/ In a0 [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' (list_repeat' [] a n)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="array-v-chk69" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">a' <> a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a0</span> : A, +In a0 (list_repeat' [] a n ++ [a]) -> +In a0 (list_repeat' [] a n) \/ In a0 [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' [a]</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="array-v-chk69"><hr></label><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk6a" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk6a"><span class="highlight">-</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">a' <> a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a0</span> : A, +In a0 (list_repeat' [] a n ++ [a]) -> +In a0 (list_repeat' [] a n) \/ In a0 [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' (list_repeat' [] a n)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">eapply</span> IHn <span class="kr">in</span> X; <span class="bp">eassumption</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk6b" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk6b"><span class="highlight">-</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a</span> <span class="nv">a'</span> : A, +(<span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}) -> +In a' (list_repeat' [] a n) -> a' = a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a, a'</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">X</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">x</span> <span class="nv">x'</span> : A, {x' = x} + {x' <> x}</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">a' <> a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">a0</span> : A, +In a0 (list_repeat' [] a n ++ [a]) -> +In a0 (list_repeat' [] a n) \/ In a0 [a]</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H1</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">In a' [a]</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">a' = a</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight">invert H1; <span class="bp">contradiction</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk6c" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk6c"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_repeat_head_tail</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : <span class="kr">forall</span> <span class="nv">n</span> (<span class="nv">a</span> : A), + a :: list_repeat a n = list_repeat a n ++ [a].</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), +a :: list_repeat a n = list_repeat a n ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk6d" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk6d"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), +a :: list_repeat a n = list_repeat a n ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk6e" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk6e"><span class="highlight"><span class="nb">unfold</span> list_repeat.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), +a :: list_repeat' [] a n = list_repeat' [] a n ++ [a]</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">apply</span> list_repeat'_head_tail.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk6f" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk6f"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_repeat_cons</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : <span class="kr">forall</span> <span class="nv">n</span> (<span class="nv">a</span> : A), + list_repeat a (S n) = a :: list_repeat a n.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), +list_repeat a (S n) = a :: list_repeat a n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk70" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk70"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), +list_repeat a (S n) = a :: list_repeat a n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk71" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk71"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat a (S n) = a :: list_repeat a n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk72" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk72"><span class="highlight"><span class="nb">unfold</span> list_repeat.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">list_repeat' [] a (S n) = a :: list_repeat' [] a n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">apply</span> list_repeat'_cons.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk73" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk73"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_repeat_lookup</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : + <span class="kr">forall</span> <span class="nv">n</span> <span class="nv">i</span> (<span class="nv">a</span> : A), + i < n -> + nth_error (list_repeat a n) i = Some a.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> <span class="nv">i</span> : nat) (<span class="nv">a</span> : A), +i < n -> nth_error (list_repeat a n) i = Some a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk74" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk74"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> <span class="nv">i</span> : nat) (<span class="nv">a</span> : A), +i < n -> nth_error (list_repeat a n) i = Some a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk75" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk75"><span class="highlight"><span class="nb">induction</span> n; <span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < <span class="mi">0</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (list_repeat a <span class="mi">0</span>) i = Some a</span></div></blockquote><div class="coq-extra-goals"><input class="coq-extra-goal-toggle" id="array-v-chk76" style="display: none" type="checkbox"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> (<span class="nv">i</span> : nat) (<span class="nv">a</span> : A), i < n -> nth_error (list_repeat a n) i = Some a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < S n</span></span></span></span></div></div><label class="goal-separator coq-extra-goal-label" for="array-v-chk76"><hr></label><div class="goal-conclusion"><span class="highlight">nth_error (list_repeat a (S n)) i = Some a</span></div></blockquote></div></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk77" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk77"><span class="highlight"><span class="nb">destruct</span> i; crush.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> (<span class="nv">i</span> : nat) (<span class="nv">a</span> : A), i < n -> nth_error (list_repeat a n) i = Some a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < S n</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (list_repeat a (S n)) i = Some a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk78" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk78"><span class="highlight"><span class="nb">rewrite</span> list_repeat_cons.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> (<span class="nv">i</span> : nat) (<span class="nv">a</span> : A), i < n -> nth_error (list_repeat a n) i = Some a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">i < S n</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (a :: list_repeat a n) i = Some a</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk79" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk79"><span class="highlight"><span class="nb">destruct</span> i; crush; <span class="nb">firstorder</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHn</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> (<span class="nv">i</span> : nat) (<span class="nv">a</span> : A), i < n -> nth_error (list_repeat a n) i = Some a</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">i</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">S i < S n</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">nth_error (list_repeat a n) i = Some a</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">intuition</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">arr_repeat</span> {<span class="nv">A</span> : <span class="kt">Type</span>} (<span class="nv">a</span> : A) (<span class="nv">n</span> : nat) : Array A := make_array (list_repeat a n).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk7a" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk7a"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">arr_repeat_length</span> {<span class="nv">A</span> : <span class="kt">Type</span>} : <span class="kr">forall</span> <span class="nv">n</span> (<span class="nv">a</span> : A), arr_length (arr_repeat a n) = n.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), +arr_length (arr_repeat a n) = n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk7b" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk7b"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), +arr_length (arr_repeat a n) = n</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk7c" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk7c"><span class="highlight"><span class="nb">unfold</span> list_repeat.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">n</span> : nat) (<span class="nv">a</span> : A), +arr_length (arr_repeat a n) = n</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk7d" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk7d"><span class="highlight">crush.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">n</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">nat</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length (list_repeat a n) = n</span></div></blockquote></div></div></small><span class="coq-wsp"> </span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">apply</span> list_repeat_len.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Fixpoint</span> <span class="nf">list_combine</span> {<span class="nv">A</span> <span class="nv">B</span> <span class="nv">C</span> : <span class="kt">Type</span>} (<span class="nv">f</span> : A -> B -> C) (<span class="nv">x</span> : list A) (<span class="nv">y</span> : list B) : list C := + <span class="kr">match</span> x, y <span class="kr">with</span> + | a :: t, b :: t' => f a b :: list_combine f t t' + | _, _ => nil + <span class="kr">end</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk7e" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk7e"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">list_combine_length</span> {<span class="nv">A</span> <span class="nv">B</span> <span class="nv">C</span> : <span class="kt">Type</span>} (<span class="nv">f</span> : A -> B -> C) : <span class="kr">forall</span> (<span class="nv">x</span> : list A) (<span class="nv">y</span> : list B), + length (list_combine f x y) = min (length x) (length y).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">x</span> : list A) (<span class="nv">y</span> : list B), +length (list_combine f x y) = +Init.Nat.min (length x) (length y)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk7f" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk7f"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">x</span> : list A) (<span class="nv">y</span> : list B), +length (list_combine f x y) = +Init.Nat.min (length x) (length y)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk80" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk80"><span class="highlight"><span class="nb">induction</span> x; <span class="nb">intros</span>; crush.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">IHx</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kr">forall</span> <span class="nv">y</span> : list B, +length (list_combine f x y) = Init.Nat.min (length x) (length y)</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">y</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list B</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length + <span class="kr">match</span> y <span class="kr">with</span> + | [] => [] + | b :: t' => f a b :: list_combine f x t' + <span class="kr">end</span> = +<span class="kr">match</span> length y <span class="kr">with</span> +| <span class="mi">0</span> => <span class="mi">0</span> +| S m' => S (Init.Nat.min (length x) m') +<span class="kr">end</span></span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">destruct</span> y; crush; <span class="nb">auto</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Definition</span> <span class="nf">combine</span> {<span class="nv">A</span> <span class="nv">B</span> <span class="nv">C</span> : <span class="kt">Type</span>} (<span class="nv">f</span> : A -> B -> C) (<span class="nv">x</span> : Array A) (<span class="nv">y</span> : Array B) : Array C := + make_array (list_combine f x.(arr_contents) y.(arr_contents)).</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk81" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk81"><span class="highlight"><span class="kn">Lemma</span> <span class="nf">combine_length</span> {<span class="nv">A</span> <span class="nv">B</span> <span class="nv">C</span>: <span class="kt">Type</span>} : <span class="kr">forall</span> <span class="nv">x</span> <span class="nv">y</span> (<span class="nv">f</span> : A -> B -> C), + x.(arr_length) = y.(arr_length) -> arr_length (combine f x y) = x.(arr_length).</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">x</span> : Array A) (<span class="nv">y</span> : Array B) (<span class="nv">f</span> : A -> B -> C), +arr_length x = arr_length y -> +arr_length (combine f x y) = arr_length x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk82" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk82"><span class="highlight"><span class="kn">Proof</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight"><span class="kr">forall</span> (<span class="nv">x</span> : Array A) (<span class="nv">y</span> : Array B) (<span class="nv">f</span> : A -> B -> C), +arr_length x = arr_length y -> +arr_length (combine f x y) = arr_length x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk83" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk83"><span class="highlight"><span class="nb">intros</span>.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">y</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">arr_length x = arr_length y</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">arr_length (combine f x y) = arr_length x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk84" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk84"><span class="highlight"><span class="nb">unfold</span> combine.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">y</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">arr_length x = arr_length y</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">arr_length + (make_array + (list_combine f (arr_contents x) (arr_contents y))) = +arr_length x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk85" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk85"><span class="highlight"><span class="nb">unfold</span> make_array.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">y</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">arr_length x = arr_length y</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">arr_length + {| + arr_contents := list_combine f (arr_contents x) + (arr_contents y); + arr_length := length + (list_combine f (arr_contents x) + (arr_contents y)); + arr_wf := eq_refl |} = arr_length x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk86" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk86"><span class="highlight">crush.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">y</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">arr_length x = arr_length y</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length + (list_combine f (arr_contents x) (arr_contents y)) = +arr_length x</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk87" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk87"><span class="highlight"><span class="nb">rewrite</span> <- (arr_wf x) <span class="kr">in</span> *.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">y</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">length (arr_contents x) = arr_length y</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length + (list_combine f (arr_contents x) (arr_contents y)) = +length (arr_contents x)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk88" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk88"><span class="highlight"><span class="nb">rewrite</span> <- (arr_wf y) <span class="kr">in</span> *.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">y</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">length (arr_contents x) = length (arr_contents y)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length + (list_combine f (arr_contents x) (arr_contents y)) = +length (arr_contents x)</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk89" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk89"><span class="highlight"><span class="nb">destruct</span> (arr_contents x); <span class="nb">destruct</span> (arr_contents y); crush.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">y</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">b</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">S (length l) = S (length l0)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">length (list_combine f l l0) = length l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><input class="coq-toggle" id="array-v-chk8a" style="display: none" type="checkbox"><label class="coq-input" for="array-v-chk8a"><span class="highlight"><span class="nb">rewrite</span> list_combine_length.</span></label><small class="coq-output"><div class="coq-output-sticky-wrapper"><div class="coq-goals"><blockquote class="coq-goal"><div class="goal-hyps"><div class="goal-hyp"><span class="hyp-names">A, B, C</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight"><span class="kt">Type</span></span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">x</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">y</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">Array B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">f</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A -> B -> C</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">a</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list A</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">b</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">l0</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">list B</span></span></span></span></div><div class="goal-hyp"><span class="hyp-names">H</span><span><span class="hyp-type-block"><span class="hyp-punct">:</span><span class="hyp-type"><span class="highlight">S (length l) = S (length l0)</span></span></span></span></div></div><span class="goal-separator"><hr></span><div class="goal-conclusion"><span class="highlight">Init.Nat.min (length l) (length l0) = length l</span></div></blockquote></div></div></small><span class="coq-wsp"> +</span></span><span class="coq-wsp"> </span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="nb">destruct</span> (Min.min_dec (length l) (length l0)); <span class="bp">congruence</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Qed</span>.</span></span><span class="coq-wsp"> +</span></span><span class="coq-wsp"><span class="highlight"> +</span></span><span class="coq-sentence"><span class="coq-input"><span class="highlight"><span class="kn">Ltac</span> <span class="nf">array</span> := + <span class="kp">try</span> <span class="kr">match goal with</span> + | [ |- <span class="kp">context</span>[arr_length (combine _ _ _)] ] => + <span class="nb">rewrite</span> combine_length + | [ |- <span class="kp">context</span>[length (list_repeat _ _)] ] => + <span class="nb">rewrite</span> list_repeat_len + | |- <span class="kp">context</span>[array_get_error _ (arr_repeat <span class="nl">?x</span> _) = Some <span class="nl">?x</span>] => + <span class="nb">unfold</span> array_get_error, arr_repeat + | |- <span class="kp">context</span>[nth_error (list_repeat <span class="nl">?x</span> _) _ = Some <span class="nl">?x</span>] => + <span class="nb">apply</span> list_repeat_lookup + <span class="kr">end</span>.</span></span></span></pre> +</div> +</div></body> +</html> |