~/talk

Theorem Proving in Coq using Tactics

on YouTube 54m
Talkat LambdaConf Winter Retreat 2017 · 2017-01-08..01-11· [large-language-models]

speaker

name:Yawar Raza
links:none on file

resources

video:https://youtu.be/zevM27ym3qs
slides:none on file

summary

Claims and code show a machine-checked proof that the triangular sum equals n times (n+1) over 2 by defining Peano naturals and a recursive sum function and proving sum_to n = n(n+1)/2. The session uses the Coq interactive editor, deals with the decreasing-argument termination check, unfolds definitions and applies induction plus reflexivity/simpl/auto* tactics, and produces a compiled theorem usable as a lemma in later developments.

AI-written summary · about

chapters (13)

  1. 0:00Coq and theorem proving
  2. 1:00Why Coq for proofs
  3. 6:03Proofs by induction in Coq
  4. 7:57Natural numbers in Coq
  5. 11:35Triangular numbers function
  6. 22:15Termination in Coq
  7. 24:04Refining triangular sum
  8. 31:41Theorem statement
  9. 37:21Propositions as types
  10. 42:02Proof state and hypotheses
  11. 46:23Induction tactic
  12. 47:27Base case with reflexivity
  13. 51:11Inductive case usage

related talks

~/search
type to search 6,249 conferences, 138,987 speakers and 185,172 talks
~/help
cmdctrl k
search every conference, speaker and series
/
focus the filter search
h
home
c
conferences
s
speakers
e
series
t
light / dark — the status bar button does the same
?
this help
esc
close this, then clear every filter — or just the search, while you are typing in it

Ignored while you are typing. Pages without a filter rail have no search to focus.