https://github.com/uds-psl/cook-levin
Tip revision: e24a92af25746f6758a09ea1dc51e57491508e60 authored by Fabian Kunze on 03 February 2021, 23:29:51 UTC
added missing html doc
added missing html doc
Tip revision: e24a92a
Undecidability.TM.Hoare.HoareTactics.html
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="coqdoc.css" rel="stylesheet" type="text/css" />
<link href="coqdocjs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="config.js"></script>
<script type="text/javascript" src="coqdocjs.js"></script>
</head>
<body onload="document.getElementById('content').focus()">
<div id="header">
<span class="left">
<span class="modulename"> <script> document.write(document.title) </script> </span>
</span>
<span class="button" id="toggle-proofs"></span>
<span class="right">
<a href="../">Project Page</a>
<a href="./indexpage.html"> Index </a>
<a href="./toc.html"> Table of Contents </a>
</span>
</div>
<div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
<div id="main">
<div class="code">
<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Undecidability</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.TM.Compound.TMTac.html#"><span class="id" title="library">TMTac</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">Undecidability</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#"><span class="id" title="library">TM.Hoare.HoareLogic</span></a> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#"><span class="id" title="library">TM.Hoare.HoareCombinators</span></a> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#"><span class="id" title="library">TM.Hoare.HoareRegister</span></a> <a class="idref" href="Undecidability.TM.Hoare.HoareTacticsView.html#"><span class="id" title="library">TM.Hoare.HoareTacticsView</span></a>.<br/>
<span class="id" title="keyword">From</span> <span class="id" title="var">smpl</span> <span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <span class="id" title="library">Smpl</span>.<br/>
<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">contains_evar</span> <span class="id" title="var">e</span> := <span class="id" title="var">has_evar</span> <span class="id" title="var">e</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">triple_with_space</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <span class="id" title="keyword">context</span> [<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#withSpace"><span class="id" title="definition">withSpace</span></a>] ] => <span class="id" title="tactic">idtac</span><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<br/>
<span class="id" title="var">Smpl</span> <span class="id" title="var">Create</span> <span class="id" title="var">hstep_Spec</span>.<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_Spec</span> := <span class="id" title="var">smpl</span> <span class="id" title="var">hstep_Spec</span>.<br/>
<br/>
<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_Seq</span> :=<br/>
<span class="id" title="keyword">match</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Triple"><span class="id" title="inductive">Triple</span></a> ?<span class="id" title="var">P</span> (?<span class="id" title="var">M1</span><a class="idref" href="Undecidability.TM.Combinators.SequentialComposition.html#ddfa557d890d9c0cd173d40cb7db80da"><span class="id" title="notation">;;</span></a> ?<span class="id" title="var">M2</span>) ?<span class="id" title="var">Q</span> ] => <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#Seq_Spec"><span class="id" title="lemma">Seq_Spec</span></a><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> ?<span class="id" title="var">P</span> ?<span class="id" title="var">k</span> (?<span class="id" title="var">M1</span><a class="idref" href="Undecidability.TM.Combinators.SequentialComposition.html#ddfa557d890d9c0cd173d40cb7db80da"><span class="id" title="notation">;;</span></a> ?<span class="id" title="var">M2</span>) ?<span class="id" title="var">Q</span> ] => <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#Seq_SpecT"><span class="id" title="lemma">Seq_SpecT</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_If</span> :=<br/>
<span class="id" title="var">cbn</span> <span class="id" title="keyword">beta</span>;<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Triple"><span class="id" title="inductive">Triple</span></a> <span class="id" title="var">_</span> (<a class="idref" href="Undecidability.TM.Combinators.If.html#If"><span class="id" title="definition">If</span></a> ?<span class="id" title="var">M1</span> ?<span class="id" title="var">M2</span> ?<span class="id" title="var">M3</span>) <span class="id" title="var">_</span> ] => <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#If_Spec"><span class="id" title="lemma">If_Spec</span></a><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#3172a2a4bf82cf37aae3076a31134f03"><span class="id" title="notation">≃≃(</span></a> <span class="id" title="var">_</span><a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#3172a2a4bf82cf37aae3076a31134f03"><span class="id" title="notation">,</span></a><span class="id" title="var">_</span><a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#3172a2a4bf82cf37aae3076a31134f03"><span class="id" title="notation">)</span></a> ?<span class="id" title="var">k</span> (<a class="idref" href="Undecidability.TM.Combinators.If.html#If"><span class="id" title="definition">If</span></a> ?<span class="id" title="var">M1</span> ?<span class="id" title="var">M2</span> ?<span class="id" title="var">M3</span>) <span class="id" title="var">_</span> ] =><br/>
<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#If_SpecTReg"><span class="id" title="lemma">If_SpecTReg</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">R</span>:= <span class="id" title="keyword">fun</span> <a id="y:1" class="idref" href="#y:1"><span class="id" title="binder">y</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>) (<span class="id" title="var">Q</span>:= <span class="id" title="keyword">fun</span> <a id="y:2" class="idref" href="#y:2"><span class="id" title="binder">y</span></a> => <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>)<br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> ?<span class="id" title="var">P</span> ?<span class="id" title="var">k</span> (<a class="idref" href="Undecidability.TM.Combinators.If.html#If"><span class="id" title="definition">If</span></a> ?<span class="id" title="var">M1</span> ?<span class="id" title="var">M2</span> ?<span class="id" title="var">M3</span>) ?<span class="id" title="var">Q</span> ] => <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#If_SpecT"><span class="id" title="lemma">If_SpecT</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_Switch</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Triple"><span class="id" title="inductive">Triple</span></a> ?<span class="id" title="var">P</span> (<a class="idref" href="Undecidability.TM.Combinators.Switch.html#Switch"><span class="id" title="definition">Switch</span></a> ?<span class="id" title="var">M1</span> ?<span class="id" title="var">M2</span>) ?<span class="id" title="var">Q</span> ] => <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#Switch_Spec"><span class="id" title="lemma">Switch_Spec</span></a><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> ?<span class="id" title="var">P</span> ?<span class="id" title="var">k</span> (<a class="idref" href="Undecidability.TM.Combinators.Switch.html#Switch"><span class="id" title="definition">Switch</span></a> ?<span class="id" title="var">M1</span> ?<span class="id" title="var">M2</span>) ?<span class="id" title="var">Q</span> ] => <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#Switch_SpecT"><span class="id" title="lemma">Switch_SpecT</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_Return</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Triple"><span class="id" title="inductive">Triple</span></a> ?<span class="id" title="var">P</span> (<a class="idref" href="Undecidability.TM.Combinators.Combinators.html#Return"><span class="id" title="definition">Return</span></a> ?<span class="id" title="var">M</span> ?<span class="id" title="var">x</span>) ?<span class="id" title="var">Q</span> ] =><br/>
(<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#Return_Spec_con"><span class="id" title="lemma">Return_Spec_con</span></a>)<br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> ?<span class="id" title="var">P</span> ?<span class="id" title="var">k</span> (<a class="idref" href="Undecidability.TM.Combinators.Combinators.html#Return"><span class="id" title="definition">Return</span></a> ?<span class="id" title="var">M</span> ?<span class="id" title="var">x</span>) ?<span class="id" title="var">Q</span> ] =><br/>
(<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#Return_SpecT_con"><span class="id" title="lemma">Return_SpecT_con</span></a>)<br/>
<br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Triple"><span class="id" title="inductive">Triple</span></a> ?<span class="id" title="var">P</span> (<a class="idref" href="Undecidability.TM.Combinators.Combinators.html#Relabel"><span class="id" title="definition">Relabel</span></a> ?<span class="id" title="var">M</span> ?<span class="id" title="var">f</span>) ?<span class="id" title="var">Q</span> ] =><br/>
(<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#Relabel_Spec_con"><span class="id" title="lemma">Relabel_Spec_con</span></a>)<br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> ?<span class="id" title="var">P</span> ?<span class="id" title="var">k</span> (<a class="idref" href="Undecidability.TM.Combinators.Combinators.html#Relabel"><span class="id" title="definition">Relabel</span></a> ?<span class="id" title="var">M</span> ?<span class="id" title="var">f</span>) ?<span class="id" title="var">Q</span> ] =><br/>
(<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#Relabel_SpecT_con"><span class="id" title="lemma">Relabel_SpecT_con</span></a>)<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_LiftTapes</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Triple"><span class="id" title="inductive">Triple</span></a> ?<span class="id" title="var">PRE</span> (<a class="idref" href="Undecidability.TM.Lifting.LiftTapes.html#LiftTapes"><span class="id" title="definition">LiftTapes</span></a> ?<span class="id" title="var">M</span> ?<span class="id" title="var">I</span>) ?<span class="id" title="var">POST</span> ] =><br/>
<span class="id" title="var">tryif</span> <span class="id" title="var">contains_evar</span> <span class="id" title="var">POST</span> <span class="id" title="keyword">then</span> <br/>
(<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span><br/>
<span class="id" title="keyword">then</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#LiftTapes_Spec_space"><span class="id" title="lemma">LiftTapes_Spec_space</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">Q'</span>:= <span class="id" title="keyword">fun</span> <a id="y:17" class="idref" href="#y:17"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q</span>:= <span class="id" title="keyword">fun</span> <a id="y:18" class="idref" href="#y:18"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [<span class="id" title="var">smpl_dupfree</span> | ])<br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#LiftTapes_Spec"><span class="id" title="lemma">LiftTapes_Spec</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">Q'</span>:= <span class="id" title="keyword">fun</span> <a id="y:15" class="idref" href="#y:15"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q</span>:= <span class="id" title="keyword">fun</span> <a id="y:16" class="idref" href="#y:16"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [<span class="id" title="var">smpl_dupfree</span> | ]))<br/>
<span class="id" title="keyword">else</span> <br/>
(<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span> <span class="id" title="keyword">then</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#LiftTapes_Spec_space_con"><span class="id" title="lemma">LiftTapes_Spec_space_con</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">R'</span>:= <span class="id" title="keyword">fun</span> <a id="y:13" class="idref" href="#y:13"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">R</span>:= <span class="id" title="keyword">fun</span> <a id="y:14" class="idref" href="#y:14"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [<span class="id" title="var">smpl_dupfree</span> | | ])<br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#LiftTapes_Spec_con"><span class="id" title="lemma">LiftTapes_Spec_con</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">R'</span>:= <span class="id" title="keyword">fun</span> <a id="y:11" class="idref" href="#y:11"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">R</span>:= <span class="id" title="keyword">fun</span> <a id="y:12" class="idref" href="#y:12"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [<span class="id" title="var">smpl_dupfree</span> | | ]))<br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> ?<span class="id" title="var">PRE</span> ?<span class="id" title="var">k</span> (<a class="idref" href="Undecidability.TM.Lifting.LiftTapes.html#LiftTapes"><span class="id" title="definition">LiftTapes</span></a> ?<span class="id" title="var">M</span> ?<span class="id" title="var">I</span>) ?<span class="id" title="var">POST</span> ] =><br/>
<span class="id" title="var">tryif</span> <span class="id" title="var">contains_evar</span> <span class="id" title="var">POST</span> <span class="id" title="keyword">then</span><br/>
(<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span> <span class="id" title="keyword">then</span> (<span class="id" title="tactic">refine</span> (<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#LiftTapes_SpecT_space"><span class="id" title="lemma">LiftTapes_SpecT_space</span></a> (<span class="id" title="var">Q'</span>:= <span class="id" title="keyword">fun</span> <a id="y:10" class="idref" href="#y:10"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q</span>:= <span class="id" title="keyword">fun</span> <a id="y:9" class="idref" href="#y:9"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) <span class="id" title="var">_</span> <span class="id" title="var">_</span>); [<span class="id" title="var">smpl_dupfree</span> | ])<br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">refine</span> (<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#LiftTapes_SpecT"><span class="id" title="lemma">LiftTapes_SpecT</span></a> (<span class="id" title="var">Q'</span>:= <span class="id" title="keyword">fun</span> <a id="y:8" class="idref" href="#y:8"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q</span>:= <span class="id" title="keyword">fun</span> <a id="y:7" class="idref" href="#y:7"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) <span class="id" title="var">_</span> <span class="id" title="var">_</span>); [<span class="id" title="var">smpl_dupfree</span> | ]))<br/>
<span class="id" title="keyword">else</span><br/>
(<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span> <span class="id" title="keyword">then</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#LiftTapes_SpecT_space_con"><span class="id" title="lemma">LiftTapes_SpecT_space_con</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">R'</span>:= <span class="id" title="keyword">fun</span> <a id="y:5" class="idref" href="#y:5"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">R</span>:= <span class="id" title="keyword">fun</span> <a id="y:6" class="idref" href="#y:6"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [<span class="id" title="var">smpl_dupfree</span> | | ])<br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#LiftTapes_SpecT_con"><span class="id" title="lemma">LiftTapes_SpecT_con</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">R'</span>:= <span class="id" title="keyword">fun</span> <a id="y:3" class="idref" href="#y:3"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">R</span>:= <span class="id" title="keyword">fun</span> <a id="y:4" class="idref" href="#y:4"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [<span class="id" title="var">smpl_dupfree</span> | | ]))<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_ChangeAlphabet</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Triple"><span class="id" title="inductive">Triple</span></a> ?<span class="id" title="var">PRE</span> (<a class="idref" href="Undecidability.TM.Code.ChangeAlphabet.html#ChangeAlphabet"><span class="id" title="definition">ChangeAlphabet</span></a> ?<span class="id" title="var">M</span> ?<span class="id" title="var">I</span>)?<span class="id" title="var">POST</span> ] =><br/>
<span class="id" title="var">tryif</span> <span class="id" title="var">contains_evar</span> <span class="id" title="var">POST</span> <span class="id" title="keyword">then</span> <br/>
(<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span> <span class="id" title="keyword">then</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#ChangeAlphabet_Spec_space_pre"><span class="id" title="lemma">ChangeAlphabet_Spec_space_pre</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">Q</span>:= <span class="id" title="keyword">fun</span> <a id="y:35" class="idref" href="#y:35"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q0</span>:= <span class="id" title="keyword">fun</span> <a id="y:36" class="idref" href="#y:36"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [ | ])<br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#ChangeAlphabet_Spec_pre"><span class="id" title="lemma">ChangeAlphabet_Spec_pre</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">Q</span>:= <span class="id" title="keyword">fun</span> <a id="y:33" class="idref" href="#y:33"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q0</span>:= <span class="id" title="keyword">fun</span> <a id="y:34" class="idref" href="#y:34"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [ | ]))<br/>
<span class="id" title="keyword">else</span> <br/>
(<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span> <span class="id" title="keyword">then</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#ChangeAlphabet_Spec_space_pre_post"><span class="id" title="lemma">ChangeAlphabet_Spec_space_pre_post</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">Q'</span>:= <span class="id" title="keyword">fun</span> <a id="y:31" class="idref" href="#y:31"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q0</span>:= <span class="id" title="keyword">fun</span> <a id="y:32" class="idref" href="#y:32"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [ | | ])<br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#ChangeAlphabet_Spec_pre_post"><span class="id" title="lemma">ChangeAlphabet_Spec_pre_post</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">Q'</span>:= <span class="id" title="keyword">fun</span> <a id="y:28" class="idref" href="#y:28"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q'</span>:= <span class="id" title="keyword">fun</span> <a id="y:29" class="idref" href="#y:29"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q0</span>:= <span class="id" title="keyword">fun</span> <a id="y:30" class="idref" href="#y:30"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [ | | ]))<br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> ?<span class="id" title="var">PRE</span> ?<span class="id" title="var">k</span> (<a class="idref" href="Undecidability.TM.Code.ChangeAlphabet.html#ChangeAlphabet"><span class="id" title="definition">ChangeAlphabet</span></a> ?<span class="id" title="var">M</span> ?<span class="id" title="var">I</span>)?<span class="id" title="var">POST</span> ] =><br/>
<span class="id" title="var">tryif</span> <span class="id" title="var">contains_evar</span> <span class="id" title="var">POST</span> <span class="id" title="keyword">then</span><br/>
(<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span> <span class="id" title="keyword">then</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#ChangeAlphabet_SpecT_space_pre"><span class="id" title="lemma">ChangeAlphabet_SpecT_space_pre</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">Q</span>:= <span class="id" title="keyword">fun</span> <a id="y:26" class="idref" href="#y:26"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q0</span>:= <span class="id" title="keyword">fun</span> <a id="y:27" class="idref" href="#y:27"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [ | ])<br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#ChangeAlphabet_SpecT_pre"><span class="id" title="lemma">ChangeAlphabet_SpecT_pre</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">Q</span>:= <span class="id" title="keyword">fun</span> <a id="y:24" class="idref" href="#y:24"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q0</span>:= <span class="id" title="keyword">fun</span> <a id="y:25" class="idref" href="#y:25"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [ | ]))<br/>
<span class="id" title="keyword">else</span><br/>
(<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span> <span class="id" title="keyword">then</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#ChangeAlphabet_SpecT_space_pre_post"><span class="id" title="lemma">ChangeAlphabet_SpecT_space_pre_post</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">Q'</span>:= <span class="id" title="keyword">fun</span> <a id="y:22" class="idref" href="#y:22"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q0</span>:= <span class="id" title="keyword">fun</span> <a id="y:23" class="idref" href="#y:23"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [ | | ])<br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#ChangeAlphabet_SpecT_pre_post"><span class="id" title="lemma">ChangeAlphabet_SpecT_pre_post</span></a> <span class="id" title="keyword">with</span> (<span class="id" title="var">Q</span>:= <span class="id" title="keyword">fun</span> <a id="y:19" class="idref" href="#y:19"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q'</span>:= <span class="id" title="keyword">fun</span> <a id="y:20" class="idref" href="#y:20"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q0</span>:= <span class="id" title="keyword">fun</span> <a id="y:21" class="idref" href="#y:21"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>); [ | | ]))<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<br/>
<br/>
<br/>
<br/>
<br/>
<span class="id" title="keyword">Local</span> <span class="id" title="keyword">Tactic</span> <span class="id" title="keyword">Notation</span> "noSpace" <span class="id" title="var">tactic</span>(<span class="id" title="var">t</span>) :=<br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">test</span> :=<br/>
<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span><br/>
<span class="id" title="keyword">then</span> <span class="id" title="tactic">fail</span><br/>
<span class="id" title="keyword">else</span> <span class="id" title="tactic">reflexivity</span><br/>
<span class="id" title="tactic">in</span><br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Triple"><span class="id" title="inductive">Triple</span></a> ?<span class="id" title="var">P</span> ?<span class="id" title="var">M</span> ?<span class="id" title="var">Q</span> ] =><br/>
<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Consequence_pre"><span class="id" title="lemma">Consequence_pre</span></a>;[<span class="id" title="var">t</span>| <span class="id" title="var">test</span> ]<br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> ?<span class="id" title="var">P</span> <span class="id" title="var">_</span> ?<span class="id" title="var">M</span> ?<span class="id" title="var">Q</span> ] => <br/>
<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#ConsequenceT_pre"><span class="id" title="lemma">ConsequenceT_pre</span></a>;[<span class="id" title="var">t</span>| <span class="id" title="var">test</span> |<span class="id" title="tactic">reflexivity</span>]<br/>
<span class="id" title="keyword">end</span> || <span class="id" title="tactic">fail</span> "could not find user-rule applicable here".<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_user</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Triple"><span class="id" title="inductive">Triple</span></a> ?<span class="id" title="var">P</span> ?<span class="id" title="var">M</span> ?<span class="id" title="var">Q</span> ] => <br/>
<span class="id" title="var">tryif</span> <span class="id" title="var">contains_evar</span> <span class="id" title="var">Q</span> <span class="id" title="keyword">then</span><br/>
(<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span> <span class="id" title="keyword">then</span><br/>
<br/>
((<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT_Triple"><span class="id" title="lemma">TripleT_Triple</span></a>; <span class="id" title="var">hstep_Spec</span>) <br/>
|| (<span class="id" title="var">hstep_Spec</span>))<br/>
<span class="id" title="keyword">else</span> ((<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT_Triple"><span class="id" title="lemma">TripleT_Triple</span></a>;<span class="id" title="tactic">refine</span> (<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#TripleT_RemoveSpace"><span class="id" title="lemma">TripleT_RemoveSpace</span></a> (<span class="id" title="var">Q</span>:=<span class="id" title="keyword">fun</span> <a id="y:41" class="idref" href="#y:41"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q'</span>:=<span class="id" title="keyword">fun</span> <a id="y:42" class="idref" href="#y:42"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) <span class="id" title="var">_</span>); <span class="id" title="var">now</span> (<span class="id" title="tactic">intros</span>; <span class="id" title="var">hstep_Spec</span>)) <br/>
|| (<span class="id" title="tactic">refine</span> (<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#TripleT_RemoveSpace"><span class="id" title="lemma">TripleT_RemoveSpace</span></a> (<span class="id" title="var">Q</span>:=<span class="id" title="keyword">fun</span> <a id="y:39" class="idref" href="#y:39"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q'</span>:=<span class="id" title="keyword">fun</span> <a id="y:40" class="idref" href="#y:40"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) <span class="id" title="var">_</span>); <span class="id" title="var">now</span> (<span class="id" title="tactic">intros</span>; <span class="id" title="var">hstep_Spec</span>)) <br/>
|| (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT_Triple"><span class="id" title="lemma">TripleT_Triple</span></a>; <span class="id" title="var">hstep_Spec</span>) <br/>
|| (<span class="id" title="var">noSpace</span> <span class="id" title="var">hstep_Spec</span>))) <br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Consequence_post"><span class="id" title="lemma">Consequence_post</span></a>; [ <span class="id" title="var">hstep_user</span> | ]) <br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> ?<span class="id" title="var">P</span> ?<span class="id" title="var">k</span> ?<span class="id" title="var">M</span> ?<span class="id" title="var">Q</span> ] => <br/>
<span class="id" title="var">tryif</span> <span class="id" title="var">contains_evar</span> <span class="id" title="var">Q</span> <span class="id" title="keyword">then</span><br/>
(<span class="id" title="var">tryif</span> <span class="id" title="var">triple_with_space</span> <span class="id" title="keyword">then</span> <span class="id" title="var">hstep_Spec</span> <br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">refine</span> (<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#TripleT_RemoveSpace"><span class="id" title="lemma">TripleT_RemoveSpace</span></a> (<span class="id" title="var">Q</span>:=<span class="id" title="keyword">fun</span> <a id="y:37" class="idref" href="#y:37"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>) (<span class="id" title="var">Q'</span>:=<span class="id" title="keyword">fun</span> <a id="y:38" class="idref" href="#y:38"><span class="id" title="binder">y</span></a> => <span class="id" title="var">_</span>)<span class="id" title="var">_</span>); <span class="id" title="var">now</span> (<span class="id" title="tactic">intros</span>; <span class="id" title="var">hstep_Spec</span>)) <br/>
|| (<span class="id" title="var">noSpace</span> <span class="id" title="var">hstep_Spec</span>))<br/>
<span class="id" title="keyword">else</span> (<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#ConsequenceT_post"><span class="id" title="lemma">ConsequenceT_post</span></a>; [ <span class="id" title="var">hstep_user</span> | ]) <br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_Nop</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
<br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> ?<span class="id" title="var">P</span> ?<span class="id" title="var">k</span> <a class="idref" href="Undecidability.TM.Compound.Multi.html#Nop"><span class="id" title="definition">Nop</span></a> ?<span class="id" title="var">Q</span> ] => <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareCombinators.html#Nop_SpecT"><span class="id" title="lemma">Nop_SpecT</span></a><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="var">Smpl</span> <span class="id" title="keyword">Add</span> <span class="id" title="var">hstep_Nop</span> : <span class="id" title="var">hstep_Spec</span>.<br/>
<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_forall_unit</span> :=<br/>
<span class="id" title="tactic">hnf</span>;<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> ?<span class="id" title="var">H</span> ] => <span class="id" title="tactic">intros</span> <span class="id" title="var">_</span><br/>
| [ |- <span class="id" title="keyword">forall</span> (<a id="y:44" class="idref" href="#y:44"><span class="id" title="binder">y</span></a> : <a class="idref" href="Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypes.html#finType_CS"><span class="id" title="definition">finType_CS</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>), ?<span class="id" title="var">H</span>] => <span class="id" title="tactic">intros</span> [] <br/>
| [ |- <span class="id" title="keyword">forall</span> (<a id="y:46" class="idref" href="#y:46"><span class="id" title="binder">y</span></a> : <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#unit"><span class="id" title="inductive">unit</span></a>), ?<span class="id" title="var">H</span>] => <span class="id" title="tactic">intros</span> []<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_pre</span> := <span class="id" title="var">clear_abbrevs</span>;<span class="id" title="var">cbn</span> <span class="id" title="keyword">beta</span>.<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_post</span> := <span class="id" title="tactic">lazy</span> <span class="id" title="keyword">beta</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_Combinators</span> := <span class="id" title="var">hstep_Seq</span> || <span class="id" title="var">hstep_If</span> || <span class="id" title="var">hstep_Switch</span> || <span class="id" title="var">hstep_Return</span>. <span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_Lifts</span> := (<span class="id" title="var">hstep_LiftTapes</span> || <span class="id" title="var">hstep_ChangeAlphabet</span>).<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep</span> := <span class="id" title="var">hstep_pre</span>; (<span class="id" title="var">hstep_forall_unit</span> || <span class="id" title="var">hstep_Combinators</span> || <span class="id" title="var">hstep_Lifts</span> || <span class="id" title="var">hstep_user</span>); <span class="id" title="var">hstep_post</span>.<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hsteps</span> := <span class="id" title="tactic">repeat</span> <span class="id" title="tactic">first</span> [<span class="id" title="var">hstep</span> | <span class="id" title="var">hstep_post</span>] .<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hsteps_cbn</span> := <span class="id" title="tactic">repeat</span> (<span class="id" title="var">cbn</span>; <span class="id" title="var">hstep</span>).
<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">openFoldRight</span> :=<br/>
<span class="id" title="tactic">try</span> (<span class="id" title="tactic">hnf</span>;<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| |- <span class="id" title="var">_</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#ba2b0e492d2b4675a0acf3ea92aabadd"><span class="id" title="notation">/\</span></a> <span class="id" title="var">_</span> => <span class="id" title="tactic">refine</span> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#conj"><span class="id" title="constructor">conj</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span>);[ | <span class="id" title="var">openFoldRight</span>]<br/>
| |- <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#True"><span class="id" title="inductive">True</span></a> => <span class="id" title="tactic">exact</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#I"><span class="id" title="constructor">I</span></a><br/>
<span class="id" title="keyword">end</span>).<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">tspec_solve</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#withSpace"><span class="id" title="definition">withSpace</span></a> <span class="id" title="var">_</span> ?<span class="id" title="var">ss</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ?<span class="id" title="var">t</span> ] => <br/>
<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec_space_solve"><span class="id" title="lemma">tspec_space_solve</span></a>;<span class="id" title="var">openFoldRight</span>;[ .. | <span class="id" title="tactic">intros</span> <span class="id" title="var">i</span>; <span class="id" title="var">destruct_fin</span> <span class="id" title="var">i</span>;<br/>
<span class="id" title="var">cbn</span> [<span class="id" title="var">tspec_single</span> <span class="id" title="var">withSpace_single</span> <span class="id" title="var">Vector.map</span> <span class="id" title="var">Vector.nth</span> <span class="id" title="var">Vector.case0</span> <span class="id" title="var">Vector.caseS</span>]; <span class="id" title="tactic">try</span> (<span class="id" title="tactic">simple</span> <span class="id" title="tactic">apply</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#I"><span class="id" title="constructor">I</span></a> || <span class="id" title="var">contains_ext</span> || <span class="id" title="var">isVoid_mono</span>)]<br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>?<span class="id" title="var">P</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a>?<span class="id" title="var">R</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ?<span class="id" title="var">t</span> ] =><br/>
<span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec_solve"><span class="id" title="lemma">tspec_solve</span></a>;<span class="id" title="var">openFoldRight</span>;[ .. | <span class="id" title="tactic">intros</span> <span class="id" title="var">i</span>; <span class="id" title="var">destruct_fin</span> <span class="id" title="var">i</span>;<br/>
<span class="id" title="var">cbn</span> [<span class="id" title="var">tspec_single</span> <span class="id" title="var">Vector.nth</span> <span class="id" title="var">Vector.case0</span> <span class="id" title="var">Vector.caseS</span>]; <span class="id" title="tactic">try</span> (<span class="id" title="tactic">simple</span> <span class="id" title="tactic">apply</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#I"><span class="id" title="constructor">I</span></a> || <span class="id" title="var">contains_ext</span> || <span class="id" title="var">isVoid_mono</span>)]<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">trySolveTrivEq</span> := <span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span> |- ?<span class="id" title="var">s</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> ?<span class="id" title="var">s</span> => <span class="id" title="tactic">reflexivity</span> | |- <span class="id" title="var">_</span> => <span class="id" title="tactic">idtac</span> <span class="id" title="keyword">end</span>.<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">tspec_ext</span> :=<br/>
<span class="id" title="var">unfold_abbrev</span>;<span class="id" title="tactic">intros</span>;<br/>
<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| [ |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Entails"><span class="id" title="inductive">Entails</span></a> (<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> <span class="id" title="var">_</span>) (<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> <span class="id" title="var">_</span>) ] => <span class="id" title="tactic">simple</span> <span class="id" title="tactic">apply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#EntailsI"><span class="id" title="constructor">EntailsI</span></a>;<span class="id" title="tactic">intros</span> ? ?; <span class="id" title="var">tspec_ext</span><br/>
| [ |- <span class="id" title="keyword">forall</span> <a id="t:48" class="idref" href="#t:48"><span class="id" title="binder">t</span></a>, <a class="idref" href="Undecidability.TM.Hoare.HoareTactics.html#t:47"><span class="id" title="variable">t</span></a> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#be2a5283fbc93ea634da8c4b627b16d5"><span class="id" title="notation">≃≃</span></a> ?<span class="id" title="var">P</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#::type_scope:x_'->'_x"><span class="id" title="notation">-></span></a> <a class="idref" href="Undecidability.TM.Hoare.HoareTactics.html#t:47"><span class="id" title="variable">t</span></a> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#be2a5283fbc93ea634da8c4b627b16d5"><span class="id" title="notation">≃≃</span></a> ?<span class="id" title="var">Q</span> ] => <br/>
<span class="id" title="keyword">let</span> <span class="id" title="var">Ht</span> := <span class="id" title="tactic">fresh</span> "H"<span class="id" title="var">t</span> <span class="id" title="tactic">in</span><br/>
<span class="id" title="tactic">intros</span> <span class="id" title="var">t</span> <span class="id" title="var">Ht</span>; <span class="id" title="var">tspec_ext</span>; <span class="id" title="tactic">eauto</span><br/>
| [ <span class="id" title="var">H</span> : <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#withSpace"><span class="id" title="definition">withSpace</span></a> <span class="id" title="var">_</span> ?<span class="id" title="var">ss</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ?<span class="id" title="var">t</span> |- <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#withSpace"><span class="id" title="definition">withSpace</span></a> <span class="id" title="var">_</span> ?<span class="id" title="var">ss'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ?<span class="id" title="var">t</span> ] =><br/>
<span class="id" title="tactic">apply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec_space_ext"><span class="id" title="lemma">tspec_space_ext</span></a> <span class="id" title="keyword">with</span> (1 := <span class="id" title="var">H</span>);[ <span class="id" title="var">cbn</span> [<span class="id" title="var">implList</span>];<span class="id" title="tactic">intros</span>; <span class="id" title="var">openFoldRight</span>;<span class="id" title="var">trySolveTrivEq</span> |<br/>
((<span class="id" title="var">now</span> <span class="id" title="tactic">eauto</span>)<br/>
|| (<span class="id" title="tactic">intros</span> <span class="id" title="var">i</span>; <span class="id" title="var">destruct_fin</span> <span class="id" title="var">i</span>;<br/>
<span class="id" title="var">cbn</span> [<span class="id" title="var">tspec_single</span> <span class="id" title="var">withSpace_single</span> <span class="id" title="var">Vector.nth</span> <span class="id" title="var">Vector.case0</span> <span class="id" title="var">Vector.caseS</span>];<br/>
<span class="id" title="tactic">intros</span>; <span class="id" title="tactic">try</span> (<span class="id" title="tactic">simple</span> <span class="id" title="tactic">apply</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#I"><span class="id" title="constructor">I</span></a> ||<span class="id" title="var">contains_ext</span> || <span class="id" title="var">isVoid_mono</span>)))]<br/>
| [ <span class="id" title="var">H</span> : <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>?<span class="id" title="var">P'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a>?<span class="id" title="var">R'</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ?<span class="id" title="var">t</span> |- <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>?<span class="id" title="var">P</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a>?<span class="id" title="var">R</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a> ?<span class="id" title="var">t</span> ] => <br/>
<span class="id" title="tactic">apply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec_ext"><span class="id" title="lemma">tspec_ext</span></a> <span class="id" title="keyword">with</span> (1 := <span class="id" title="var">H</span>);[ <span class="id" title="var">cbn</span> [<span class="id" title="var">implList</span>];<span class="id" title="tactic">intros</span>; <span class="id" title="var">openFoldRight</span>;<span class="id" title="var">trySolveTrivEq</span> |<br/>
((<span class="id" title="var">now</span> <span class="id" title="tactic">eauto</span>)<br/>
|| (<span class="id" title="tactic">intros</span> <span class="id" title="var">i</span>; <span class="id" title="var">destruct_fin</span> <span class="id" title="var">i</span>;<br/>
<span class="id" title="var">cbn</span> [<span class="id" title="var">tspec_single</span> <span class="id" title="var">Vector.nth</span> <span class="id" title="var">Vector.case0</span> <span class="id" title="var">Vector.caseS</span>];<br/>
<span class="id" title="tactic">intros</span>; <span class="id" title="tactic">try</span> (<span class="id" title="tactic">simple</span> <span class="id" title="tactic">apply</span> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Logic.html#I"><span class="id" title="constructor">I</span></a> || <span class="id" title="var">contains_ext</span> || <span class="id" title="var">isVoid_mono</span>)))]<br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">underBinders</span> <span class="id" title="var">t</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| |- <span class="id" title="keyword">forall</span> <a id="x:50" class="idref" href="#x:50"><span class="id" title="binder">x</span></a>, <span class="id" title="var">_</span> => <span class="id" title="keyword">let</span> <span class="id" title="var">x</span> := <span class="id" title="tactic">fresh</span> <span class="id" title="var">x</span> <span class="id" title="tactic">in</span> <span class="id" title="tactic">intros</span> <span class="id" title="var">x</span>;<span class="id" title="var">underBinders</span> <span class="id" title="var">t</span>;<span class="id" title="var">revert</span> <span class="id" title="var">x</span><br/>
| |- <span class="id" title="var">_</span> => <span class="id" title="var">t</span><br/>
<span class="id" title="keyword">end</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">introPure_prepare</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Entails"><span class="id" title="inductive">Entails</span></a> (<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> (<a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>)) <span class="id" title="var">_</span> => <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec_introPure"><span class="id" title="lemma">tspec_introPure</span></a><br/>
| |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#Triple"><span class="id" title="inductive">Triple</span></a> (<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>?<span class="id" title="var">P</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>) <span class="id" title="var">_</span> <span class="id" title="var">_</span> => <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#Triple_introPure"><span class="id" title="lemma">Triple_introPure</span></a><br/>
| |- <a class="idref" href="Undecidability.TM.Hoare.HoareLogic.html#TripleT"><span class="id" title="inductive">TripleT</span></a> (<a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#tspec"><span class="id" title="definition">tspec</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">(</span></a>?<span class="id" title="var">P</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">,</span></a><span class="id" title="var">_</span><a class="idref" href="http://coq.inria.fr/distrib/V8.12.1/stdlib//Coq.Init.Datatypes.html#e6756e10c36f149b18b4a8741ed83079"><span class="id" title="notation">)</span></a>) <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> => <span class="id" title="tactic">eapply</span> <a class="idref" href="Undecidability.TM.Hoare.HoareRegister.html#TripleT_introPure"><span class="id" title="lemma">TripleT_introPure</span></a><br/>
<span class="id" title="keyword">end</span>;<span class="id" title="tactic">simpl</span> <span class="id" title="var">implList</span> <span class="id" title="tactic">at</span> 1.<br/>
<br/>
<span class="id" title="keyword">Tactic Notation</span> "hintros" <span class="id" title="var">simple_intropattern_list</span>(<span class="id" title="var">pat</span>) := <span class="id" title="var">underBinders</span> <span class="id" title="var">introPure_prepare</span>;<span class="id" title="tactic">intros</span> <span class="id" title="var">pat</span>.<br/>
<br/>
<span class="id" title="keyword">Ltac</span> <span class="id" title="var">hstep_seq</span> :=<br/>
<span class="id" title="keyword">lazymatch</span> <span class="id" title="keyword">goal</span> <span class="id" title="keyword">with</span><br/>
| |- ?<span class="id" title="var">R</span> (<span class="id" title="var">_</span><a class="idref" href="Undecidability.TM.Combinators.SequentialComposition.html#ddfa557d890d9c0cd173d40cb7db80da"><span class="id" title="notation">;;</span></a><span class="id" title="var">_</span>) <span class="id" title="var">_</span> => <span class="id" title="var">hstep</span>;[(<span class="id" title="var">hstep</span>;<span class="id" title="var">hsteps_cbn</span>;<span class="id" title="var">cbn</span>);<span class="id" title="keyword">let</span> <span class="id" title="var">n</span> := <span class="id" title="var">numgoals</span> <span class="id" title="tactic">in</span> (<span class="id" title="var">tryif</span> ( <span class="id" title="var">guard</span> <span class="id" title="var">n</span> = 1) <span class="id" title="keyword">then</span> <span class="id" title="tactic">try</span> <span class="id" title="var">tspec_ext</span> <span class="id" title="keyword">else</span> <span class="id" title="tactic">idtac</span> ) |<span class="id" title="var">cbn</span>;<span class="id" title="tactic">try</span> <span class="id" title="var">hstep_forall_unit</span> | <span class="id" title="tactic">reflexivity</span>..]<br/>
| |- ?<span class="id" title="var">R</span> (<a class="idref" href="Undecidability.TM.Lifting.LiftTapes.html#LiftTapes"><span class="id" title="definition">LiftTapes</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span>) <span class="id" title="var">_</span> => <span class="id" title="var">hsteps_cbn</span><br/>
| |- ?<span class="id" title="var">R</span> (<a class="idref" href="Undecidability.TM.Code.ChangeAlphabet.html#ChangeAlphabet"><span class="id" title="definition">ChangeAlphabet</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span>) <span class="id" title="var">_</span> => <span class="id" title="var">hsteps_cbn</span><br/>
<span class="id" title="keyword">end</span>.<br/>
</div>
</div>
<div id="footer">
Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>
</html>
