Deploying to gh-pages from @ 7a00839 🚀

Mcltt.Core.Completeness.FunctionCases.html

@@ -106,7 +106,12 @@ <h1 class="libtitle">Mcltt.Core.Completeness.FunctionCases</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><span class="id" title="keyword">forall</span> <a id="c:117" class="idref" href="#c:117"><span class="id" title="binder">c</span></a> <a id="c':118" class="idref" href="#c':118"><span class="id" title="binder">c'</span></a>,<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#R:115"><span class="id" title="variable">R</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#c:117"><span class="id" title="variable">c</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#c':118"><span class="id" title="variable">c'</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Mcltt.Core.Completeness.LogicalRelation.Definitions.html#rel_exp"><span class="id" title="inductive">rel_exp</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#B:112"><span class="id" title="variable">B</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">d</span></a><a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">{{{</span></a> <a id="o:119" class="idref" href="#o:119"><span class="id" title="binder"><span id="o:120" class="id">o</span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#fbe5fae0c43896171f9245ee5c9f28cb"><span class="id" title="notation">↦</span></a> <a id="c:121" class="idref" href="#c:121"><span class="id" title="binder"><span id="c:122" class="id">c</span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">}}}</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#B':114"><span class="id" title="variable">B'</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">d</span></a><a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">{{{</span></a> <a id="o':123" class="idref" href="#o':123"><span class="id" title="binder"><span id="o':124" class="id">o'</span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#fbe5fae0c43896171f9245ee5c9f28cb"><span class="id" title="notation">↦</span></a> <a id="c':125" class="idref" href="#c':125"><span class="id" title="binder"><span id="c':126" class="id">c'</span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">}}}</span></a> (<a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#per_univ"><span class="id" title="definition">per_univ</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#i:110"><span class="id" title="variable">i</span></a>)<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;We&nbsp;use&nbsp;this&nbsp;equality&nbsp;to&nbsp;make&nbsp;unification&nbsp;on&nbsp;`out_rel`&nbsp;works&nbsp;*)</span><br/>
+&nbsp;&nbsp;&nbsp;&nbsp;</div>
+
+<div class="doc">
+We use the next equality to make unification on `out_rel` works 
+</div>
+<div class="code">
 &nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">(</span></a><a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#out_rel:116"><span class="id" title="variable">out_rel</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <span class="id" title="keyword">fun</span> <a id="c:127" class="idref" href="#c:127"><span class="id" title="binder">c</span></a> <a id="c':128" class="idref" href="#c':128"><span class="id" title="binder">c'</span></a> (<a id="equiv_c_c':129" class="idref" href="#equiv_c_c':129"><span class="id" title="binder">equiv_c_c'</span></a> : <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#R:115"><span class="id" title="variable">R</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#c:127"><span class="id" title="variable">c</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#c':128"><span class="id" title="variable">c'</span></a>) <a id="m:130" class="idref" href="#m:130"><span class="id" title="binder">m</span></a> <a id="m':131" class="idref" href="#m':131"><span class="id" title="binder">m'</span></a> =&gt;<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">forall</span> <a id="R':132" class="idref" href="#R':132"><span class="id" title="binder">R'</span></a>,<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#rel_typ"><span class="id" title="definition">rel_typ</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#i:110"><span class="id" title="variable">i</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#B:112"><span class="id" title="variable">B</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">d</span></a><a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">{{{</span></a> <a id="o:133" class="idref" href="#o:133"><span class="id" title="binder"><span id="o:134" class="id">o</span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#fbe5fae0c43896171f9245ee5c9f28cb"><span class="id" title="notation">↦</span></a> <a id="c:135" class="idref" href="#c:135"><span class="id" title="binder"><span id="c:136" class="id">c</span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">}}}</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#B':114"><span class="id" title="variable">B'</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">d</span></a><a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">{{{</span></a> <a id="o':137" class="idref" href="#o':137"><span class="id" title="binder"><span id="o':138" class="id">o'</span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#fbe5fae0c43896171f9245ee5c9f28cb"><span class="id" title="notation">↦</span></a> <a id="c':139" class="idref" href="#c':139"><span class="id" title="binder"><span id="c':140" class="id">c'</span></span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#9ec978b188eee4943b90057a597432c2"><span class="id" title="notation">}}}</span></a> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#R':132"><span class="id" title="variable">R'</span></a> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Logic.html#::type_scope:x_'-&gt;'_x"><span class="id" title="notation">-&gt;</span></a><br/>
@@ -145,8 +150,7 @@ <h1 class="libtitle">Mcltt.Core.Completeness.FunctionCases</h1>
 &nbsp;&nbsp;- <span class="id" title="tactic">intros</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">eapply</span> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#rel_exp_pi_core"><span class="id" title="lemma">rel_exp_pi_core</span></a>; <span class="id" title="tactic">eauto</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">reflexivity</span>.<br/>
-&nbsp;&nbsp;- <span class="comment">(*&nbsp;`reflexivity`&nbsp;does&nbsp;not&nbsp;work&nbsp;as&nbsp;(simple)&nbsp;unification&nbsp;fails&nbsp;for&nbsp;some&nbsp;unknown&nbsp;reason.&nbsp;*)</span><br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.RelationClasses.html#Equivalence_Reflexive"><span class="id" title="method">Equivalence_Reflexive</span></a>.<br/>
+&nbsp;&nbsp;- <span class="id" title="var">solve_refl</span>.<br/>
 <span class="id" title="keyword">Qed</span>.<br/>
 
 <br/>
@@ -179,8 +183,7 @@ <h1 class="libtitle">Mcltt.Core.Completeness.FunctionCases</h1>
 &nbsp;&nbsp;- <span class="id" title="tactic">eapply</span> <a class="idref" href="Mcltt.Core.Completeness.FunctionCases.html#rel_exp_pi_core"><span class="id" title="lemma">rel_exp_pi_core</span></a>; <span class="id" title="tactic">eauto</span>; <span class="id" title="tactic">try</span> <span class="id" title="tactic">reflexivity</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">intros</span>.<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="var">extract_output_info_with</span> ρσ <span class="id" title="var">c</span> ρ'σ' <span class="id" title="var">c'</span> <span class="id" title="var">env_relΔA</span>...<br/>
-&nbsp;&nbsp;- <span class="comment">(*&nbsp;`reflexivity`&nbsp;does&nbsp;not&nbsp;work&nbsp;as&nbsp;(simple)&nbsp;unification&nbsp;fails&nbsp;for&nbsp;some&nbsp;unknown&nbsp;reason.&nbsp;*)</span><br/>
-&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">apply</span> <a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Classes.RelationClasses.html#Equivalence_Reflexive"><span class="id" title="method">Equivalence_Reflexive</span></a>.<br/>
+&nbsp;&nbsp;- <span class="id" title="var">solve_refl</span>.<br/>
 <span class="id" title="keyword">Qed</span>.<br/>
 
 <br/>

Mcltt.Core.Completeness.SubtypingCases.html

@@ -137,7 +137,12 @@ <h1 class="libtitle">Mcltt.Core.Completeness.SubtypingCases</h1>
 &nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="tactic">by</span> (<span class="id" title="tactic">intros</span>; <span class="id" title="var">apply_relation_equivalence</span>; <span class="id" title="var">unshelve</span> <span class="id" title="tactic">eexists</span>; <span class="id" title="var">eassumption</span>).<br/>
 
 <br/>
-&nbsp;&nbsp;<span class="comment">(*&nbsp;The&nbsp;proofs&nbsp;for&nbsp;the&nbsp;next&nbsp;two&nbsp;assertions&nbsp;are&nbsp;basically&nbsp;the&nbsp;same&nbsp;*)</span><br/>
+</div>
+
+<div class="doc">
+The proofs for the next two assertions are basically the same 
+</div>
+<div class="code">
 &nbsp;&nbsp;<span class="id" title="var">exvar</span> (<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Relations.Relation_Definitions.html#relation"><span class="id" title="definition">relation</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#domain"><span class="id" title="inductive">domain</span></a>)<br/>
 &nbsp;&nbsp;&nbsp;&nbsp;<span class="id" title="keyword">ltac</span>:(<span class="id" title="keyword">fun</span> <span class="id" title="var">R</span> =&gt; <span class="id" title="tactic">assert</span> (<a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">{{</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#133d1fcce1c072b503f04b70aa308ae0"><span class="id" title="notation">DF</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#e756f59cf22348e824d2c88e93573413"><span class="id" title="notation">Π</span></a> <a id="m0:97" class="idref" href="#m0:97"><span class="id" title="binder"><span id="m0:98" class="id"><span id="m0:109" class="id"><span id="m0:110" class="id">m0</span></span></span></span></a> <a id="1c04c3b2e037536356977b429c524e79" class="idref" href="#1c04c3b2e037536356977b429c524e79"><span class="id" title="binder"><span id="9ef1333d243cddfa6f7dfc3222d23a34" class="id"><span id="6c4576491be0a0349951a6e182cb5277" class="id"><span id="eb2dbbca24f9c727e202a120c18ec51b" class="id">ρ</span></span></span></span></a> <a id="B:101" class="idref" href="#B:101"><span class="id" title="binder"><span id="B:102" class="id"><span id="B:113" class="id"><span id="B:114" class="id">B</span></span></span></span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#133d1fcce1c072b503f04b70aa308ae0"><span class="id" title="notation">≈</span></a> <a class="idref" href="Mcltt.Core.Semantic.Domain.html#e756f59cf22348e824d2c88e93573413"><span class="id" title="notation">Π</span></a> <a id="m1:103" class="idref" href="#m1:103"><span class="id" title="binder"><span id="m1:104" class="id"><span id="m1:115" class="id"><span id="m1:116" class="id">m1</span></span></span></span></a> <a id="4ff549c678cb634797d767fb82acf7e1" class="idref" href="#4ff549c678cb634797d767fb82acf7e1"><span class="id" title="binder"><span id="029ba22d759cc8850998746893439aa8" class="id"><span id="75b79d67f7eac739149155c68d53d612" class="id"><span id="cebddade755c196e384c10f3ac7597c6" class="id">ρ'</span></span></span></span></a> <a id="B:107" class="idref" href="#B:107"><span class="id" title="binder"><span id="B:108" class="id"><span id="B:119" class="id"><span id="B:120" class="id">B</span></span></span></span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#133d1fcce1c072b503f04b70aa308ae0"><span class="id" title="notation">∈</span></a> <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#per_univ_elem"><span class="id" title="definition">per_univ_elem</span></a> (<a class="idref" href="http://coq.inria.fr/doc/V8.20.0/stdlib//Coq.Init.Nat.html#max"><span class="id" title="definition">Nat.max</span></a> <span class="id" title="var">i</span> <span class="id" title="var">k</span>) <a class="idref" href="Mcltt.Core.Semantic.PER.Definitions.html#133d1fcce1c072b503f04b70aa308ae0"><span class="id" title="notation">↘</span></a> <span class="id" title="var">R</span> <a class="idref" href="Mcltt.Core.Base.html#2e12ae37c5a5c7396a13d7170e0de451"><span class="id" title="notation">}}</span></a>)).<br/>
 &nbsp;&nbsp;{<br/>