Interactive Theorem Proving General

This thread if for everything used to help you prove things in a machine checked fashion. Here are some questions to get the thread going: >What environment are you using? >What IDE/UI do you prefer? >What are you doing/have you done with it? Of course, questions, useful resources and other related things are welcome as well.

I have this book tucked away, might be useful for this topic

Is there a tactic in Coq to apply the same rewrite multiple times? It's annoying and hard to read to write: rewrite a; rewrite a; rewrite a.

>what environment are you using? Debian on a hp laptop, planning to move to gentoo on a ThinkPad. i3wm >What ide ui do I prefer I3wm with vim, heavily configured .vimrc using as little as possible plugins. I use alot of inoremap filetype keybindings. >what have you done with it A bunch of python scripts and a few c projects. I'm thinking of contributing to seL4 but I'm not sure when I'll be ready. I'm reading through the c book and the art of programming and I might need a book on making formally verified software. Love the pic of miku btw (muh waifu)

>>624 do 3 rewrite a. Alternatively, repeat rewrite a. Protip: learn LTac.

>what environment are you using? A computer with Gnu/Linux >What ide ui do I prefer Sublime3/Emacs >what have you done with it Porn, Programming, BI.

>What environment are you using? proofgeneral with coq (on emacs) >What IDE/UI do you prefer? proofgeneral >What are you doing/have you done with it? autism

>What environment are you using? Coq. >What IDE/UI do you prefer? I'm using spacemacs with proof-general. More specifically this layer: https://github.com/olivierverdier/spacemacs-coq >What are you doing/have you done with it? I'm currently attending a lecture about it, so mainly the exercises on the assignment sheets. I've also played around with it on my own by proving the functor, applicative and monad laws for a few types.

>>939 >>940 How did you guys get started on coq? I tried to understand it, but for some reason it seems extremely obtuse to me. Maybe I am the one that is obtuse.

>What environment are you using? Manjaro. >What IDE/UI do you prefer? Emacs. >What are you doing/have you done with it? I'm in a undergraduate research on Proof Theory. I am still studying formal proofs, but it is likely that I will implement a proof aid for N-graphs or Gaisi-Sequent Calculus. I still do not know what language to use, but I think of some functional lang. Python is a B plan.

>>960 I got started with a college course in that subject, so it was delivered to me in bite sized chunks. Maybe try to find recordings of a course online?

I'm interested in learning more about proof checkers. Is there any particularily useful book on the topic to get started?

Maybe I'll try to write some Coq tutorial someday.

I made a bubble sort in Coq in an autistic way (obviously), in the sense that the sorting algorithm returns three things: the sorted list, the proof that it is sorted and a proof it is a permutation of the input. I'm using proofgeneral in emacs. (I changed the suffix from .v to .txt because it won't upload otherwise).

FIZZBUZZ FOR THE FIZZBUZZ GOD (require coq and ocaml) (* How to use this file *) (* let's say this file is called fizzbuzz.v *) (* $ coqtop -batch -load-vernac-source fizzbuzz.v *) (* $ ocaml -init fizzbuzz.ml *) (* # foo;; *) Require Import Arith. CoInductive stream (A : Set) : Set := | scons : A -> stream A -> stream A. Parameter string : Set. Parameters fizz buzz fizzbuzz : string. Parameter n2s : nat -> string. Definition fizzstream := (cofix f (mod3 mod5 n : nat) : stream string := if (beq_nat mod3 2) then if (beq_nat mod5 4) then scons string fizzbuzz (f 0 0 (S n)) else scons string fizz (f 0 (S mod5) (S n)) else if (beq_nat mod5 4) then scons string buzz (f (S mod3) 0 (S n)) else scons string (n2s n) (f (S mod3) (S mod5) (S n))) 0 0 1. Fixpoint take {A : Set} (n : nat) (s : stream A) : list A := match n with | 0 => nil | S n => match s with | scons a s => cons a (take n s) end end. Definition foo := Eval compute in take 100 fizzstream. Extract Inductive nat => "int" [ "0" "1 +" ]. Extract Inductive list => "list" [ "[]" "(::)" ]. Extract Constant n2s => "string_of_int". Extract Constant fizz => "let f = String.make 1 in f 'f' ^ f 'i' ^ f 'z' ^ f 'z'". Extract Constant buzz => "let f = String.make 1 in f 'b' ^ f 'u' ^ f 'z' ^ f 'z'". Extract Constant fizzbuzz => "let f = String.make 1 in f 'f' ^ f 'i' ^ f 'z' ^ f 'z' ^ f 'b' ^ f 'u' ^ f 'z' ^ f 'z'". Extraction "fizzbuzz.ml" foo.

>>960 There's a book called "Certified Programming With Dependent Types" that is a good introduction to using Coq.

>>2025 Some info on what you're trying to do with this and why you're doing things would be nice (comments) :)

Hey I'm learning coq and.. to be honest It feels like kicking whales down the beach. I know how to make proofs, why is this so complicated?

>>2148 Just use Isabelle/HOL, it's supposed to be easier. Or just go with dependent-typed language...

>>2149 I'm taking a look at Isabelle. Thank you!

This course starts in a month, says anyone can email the lecturer and be involved in the mailing list. It will be legit, it's run by people doing real research https://www.cse.unsw.edu.au/~kleing/teaching/thprv-04/

>>2178 ok that page is from 2004, im a retard, although it is running again in a month so i dont know, lecture notes there will likely be useful. Newer page with new lecture notes at https://www.cse.unsw.edu.au/~cs4161/

>>2175 You could also try Agda.

>>2187 So far with Agda I've really liked the notation system. I'm following this tutorial. It's the most practical intro I've found. I like it so far. http://people.inf.elte.hu/divip/AgdaTutorial/Index.html#general-information

Would someone like to follow the excercises on this tutorial with me? >>2202

>>2202 Here is a list of Agda 2.5.2 commands for emacs: C-c C-l : Load (type check) the current buffer. C-c C-f : Jump (forward) to active hole C-c C-b : Jump (backward) to active hole C-c C-, : Show goal type, and context of current hole C-c C-. : Show goal type, context, and type of expression in the hole. C-c C-spc : Fill the hole with the given expression C-c C-r : Refine the hole C-c C-a : Search for a proof and fill it in the hole if there is at least 1. -l : list the possible proofs -s 10 -l : skip the first 10 proofs C-c C-c : Case split the given variable(s) into its possible constructors C-c C-n : Evaluate an expression C-c C-d : Infer a type for an expression C-c C-x C-d : Kill Agda - useful if agda gets a bit fussy (Can use C-c C-l to start Agda again when needed) C-c C-x C-r : Kill and restart Agda When you're writing Agda code, you can write '?' in expressions (these are holes), then do C-c C-l to load the file, and the '?' should transform into green '{ }'. Then the above commands will help you interactively fill the hole. The arguments of the commands can be written between the '{' and '}'.

http://robbertkrebbers.nl/teaching/typessummer2017/

What environment are you using? Arch with bspwm. I mainly use Agda and Coq. What IDE/UI do you prefer? Proof General What are you doing/have you done with it? I did classes in Type Theory in Agda during my undergrad. For my PhD I am working with Coq focusing on theorem proving. I found this book to be the most helpful to learn Coq: https://softwarefoundations.cis.upenn.edu/lf-current/deps.html

>>2014 Why do I see many people here forcing functional languages, i mean they are nice and make you think but what i am seing here is torture.

>>3759 >Why do I see many people here forcing functional languages, i mean they are nice and make you think but what i am seing here is torture. Functional languages have some properties (referential transparency, no side effects, etc.) that make proving the correctness of functional programs nicer than their imperative counterparts. The type systems of functional languages also map nicely into logics: https://en.wikipedia.org/wiki/Curry–Howard_correspondence