Skip to content

Instantly share code, notes, and snippets.

Avatar

Georgy Lukyanov geo2a

View GitHub Profile
@geo2a
geo2a / EquationalReasoningTacticNotation.v
Created Jan 4, 2020
Equational Reasoning in Coq using Tactic Notations
View EquationalReasoningTacticNotation.v
Tactic Notation
"`Begin " constr(lhs) := idtac.
Tactic Notation
"≡⟨ " tactic(proof) "⟩" constr(lhs) :=
(stepl lhs by proof).
Tactic Notation
"≡⟨ " tactic(proof) "⟩" constr(lhs) "`End" :=
(now stepl lhs by proof).
View coq-non-uniform-induction.md

This is a follow-up for Li-yao Xia's answer on my StackOverflow question

Thanks for your answer Li-yao! I have a couple of follow-up notes/questions:

A Fixpoint on terms indexed by function types A -> B is useless since
no subterms of any Select term are indexed by function types.
For the same reason, induction is useless on such terms.
@geo2a
geo2a / SBVMostekCountdown.hs
Created Nov 22, 2017
An unsuccessful attempt to verify a count down program using SBV.
View SBVMostekCountdown.hs
import Control.Monad.IO.Class (liftIO)
import Data.SBV
import Data.SBV.Examples.BitPrecise.Legato
prover = z3 { verbose = True
, redirectVerbose = Just "example.smt2"
, timing = PrintTiming
, printBase = 10