Skip to content

Custom tactic named "ij_injectfalse" injects False into the hypothesis

License

Notifications You must be signed in to change notification settings

master-q/coqtactic-injectfalse

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

22 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

coqtactic-injectfalse

Custom tactic named ij_injectfalse injects False into the hypothesis. But the proof occurs an error on Qed., because Coq checks the soundness of the proof.

Coq is safe!

cat /etc/os-release  | head -1
PRETTY_NAME="Debian GNU/Linux 8 (jessie)"
$ sudo apt-get install git make coq ocaml ocaml-findlib camlp5 libcoq-ocaml-dev devscripts dh-ocaml
$ git clone https://github.com/master-q/coqtactic-injectfalse.git
$ cd coqtactic-injectfalse
$ debuild -us -uc
$ ls ../*.deb
../libinjectfalse-tactics-ocaml_0.1_amd64.deb  ../libinjectfalse-tactics-ocaml-dev_0.1_amd64.deb
$ sudo dpkg -i ../libinjectfalse-tactics-ocaml*.deb
$ coqtop
Welcome to Coq 8.4pl4 (July 2014)

Coq < Declare ML Module "injectfalse".
[Loading ML file injectfalse.cmxs ... done]

Coq < Theorem plus_0_r : forall n:nat, n + 0 = n.
1 subgoal

  ============================
   forall n : nat, n + 0 = n

plus_0_r < Proof.
1 subgoal

  ============================
   forall n : nat, n + 0 = n

plus_0_r < intros n.
1 subgoal

  n : nat
  ============================
   n + 0 = n

plus_0_r < destruct n as [| n'].
2 subgoals

  ============================
   0 + 0 = 0

subgoal 2 is:
 S n' + 0 = S n'

plus_0_r < ij_injectfalse.
1 subgoal

  n' : nat
  ============================
   S n' + 0 = S n'

plus_0_r < ij_injectfalse.
No more subgoals.

plus_0_r < Show Proof.
(fun n : nat =>
 match n as n0 return (n0 + 0 = n0) with
 | 0 => False
 | S _ => False
 end)

plus_0_r < Qed.
intros n.
destruct n as [| n'].
 ij_injectfalse.

 ij_injectfalse.

Error: In pattern-matching on term "n" the branch for constructor
"0" has type "Prop" which should be "0 + 0 = 0".

About

Custom tactic named "ij_injectfalse" injects False into the hypothesis

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published