Library Coq.rtauto.Rtauto
Require Export List.
Require Export Bintree.
Require Import Bool BinPos.
Ltac clean:=
try (
simpl;
congruence).
Inductive form:
Set:=
Atom :
positive -> form
|
Arrow :
form -> form -> form
|
Bot
|
Conjunct :
form -> form -> form
|
Disjunct :
form -> form -> form.
Notation "[ n ]":=(
Atom n).
Notation "A =>> B":= (
Arrow A B) (
at level 59,
right associativity).
Notation "#" :=
Bot.
Notation "A //\\ B" := (
Conjunct A B) (
at level 57,
left associativity).
Notation "A \\// B" := (
Disjunct A B) (
at level 58,
left associativity).
Definition ctx :=
Store form.
Fixpoint pos_eq (
m n:
positive) {
struct m} :
bool :=
match m with
xI mm =>
match n with xI nn =>
pos_eq mm nn |
_ =>
false end
|
xO mm =>
match n with xO nn =>
pos_eq mm nn |
_ =>
false end
|
xH =>
match n with xH =>
true |
_ =>
false end
end.
Theorem pos_eq_refl :
forall m n,
pos_eq m n = true -> m = n.
Fixpoint form_eq (
p q:
form) {
struct p} :
bool :=
match p with
Atom m =>
match q with Atom n =>
pos_eq m n |
_ =>
false end
|
Arrow p1 p2 =>
match q with
Arrow q1 q2 =>
form_eq p1 q1 && form_eq p2 q2
|
_ =>
false end
|
Bot =>
match q with Bot =>
true |
_ =>
false end
|
Conjunct p1 p2 =>
match q with
Conjunct q1 q2 =>
form_eq p1 q1 && form_eq p2 q2
|
_ =>
false
end
|
Disjunct p1 p2 =>
match q with
Disjunct q1 q2 =>
form_eq p1 q1 && form_eq p2 q2
|
_ =>
false
end
end.
Theorem form_eq_refl:
forall p q,
form_eq p q = true -> p = q.
Section with_env.
Variable env:
Store Prop.
Fixpoint interp_form (
f:
form):
Prop :=
match f with
[n]=>
match get n env with PNone =>
True |
PSome P =>
P end
|
A =>> B =>
(interp_form A) -> (interp_form B)
|
# =>
False
|
A //\\ B =>
(interp_form A) /\ (interp_form B)
|
A \\// B =>
(interp_form A) \/ (interp_form B)
end.
Notation "[[ A ]]" := (
interp_form A).
Fixpoint interp_ctx (
hyps:
ctx) (
F:
Full hyps) (
G:
Prop) {
struct F} :
Prop :=
match F with
F_empty =>
G
|
F_push H hyps0 F0 =>
interp_ctx hyps0 F0 (
[[H]] -> G)
end.
Ltac wipe :=
intros;
simpl;
constructor.
Lemma compose0 :
forall hyps F (
A:
Prop),
A ->
(interp_ctx hyps F A).
Lemma compose1 :
forall hyps F (
A B:
Prop),
(A -> B) ->
(interp_ctx hyps F A) ->
(interp_ctx hyps F B).
Theorem compose2 :
forall hyps F (
A B C:
Prop),
(A -> B -> C) ->
(interp_ctx hyps F A) ->
(interp_ctx hyps F B) ->
(interp_ctx hyps F C).
Theorem compose3 :
forall hyps F (
A B C D:
Prop),
(A -> B -> C -> D) ->
(interp_ctx hyps F A) ->
(interp_ctx hyps F B) ->
(interp_ctx hyps F C) ->
(interp_ctx hyps F D).
Lemma weaken :
forall hyps F f G,
(interp_ctx hyps F G) ->
(interp_ctx (
hyps\f) (
F_push f hyps F)
G).
Theorem project_In :
forall hyps F g,
In g hyps F ->
interp_ctx hyps F [[g]].
Theorem project :
forall hyps F p g,
get p hyps = PSome g->
interp_ctx hyps F [[g]].
Inductive proof:
Set :=
Ax :
positive -> proof
|
I_Arrow :
proof -> proof
|
E_Arrow :
positive -> positive -> proof -> proof
|
D_Arrow :
positive -> proof -> proof -> proof
|
E_False :
positive -> proof
|
I_And:
proof -> proof -> proof
|
E_And:
positive -> proof -> proof
|
D_And:
positive -> proof -> proof
|
I_Or_l:
proof -> proof
|
I_Or_r:
proof -> proof
|
E_Or:
positive -> proof -> proof -> proof
|
D_Or:
positive -> proof -> proof
|
Cut:
form -> proof -> proof -> proof.
Notation "hyps \ A" := (
push A hyps) (
at level 72,
left associativity).
Fixpoint check_proof (
hyps:
ctx) (
gl:
form) (
P:
proof) {
struct P}:
bool :=
match P with
Ax i =>
match get i hyps with
PSome F =>
form_eq F gl
|
_ =>
false
end
|
I_Arrow p =>
match gl with
A =>> B =>
check_proof (
hyps \ A)
B p
|
_ =>
false
end
|
E_Arrow i j p =>
match get i hyps,
get j hyps with
PSome A,
PSome (
B =>>C) =>
form_eq A B && check_proof (
hyps \ C) (
gl)
p
|
_,
_ =>
false
end
|
D_Arrow i p1 p2 =>
match get i hyps with
PSome (
(A =>>B)=>>C) =>
(check_proof (
hyps \ B =>> C \ A)
B p1) && (check_proof (
hyps \ C)
gl p2)
|
_ =>
false
end
|
E_False i =>
match get i hyps with
PSome # =>
true
|
_ =>
false
end
|
I_And p1 p2 =>
match gl with
A //\\ B =>
check_proof hyps A p1 && check_proof hyps B p2
|
_ =>
false
end
|
E_And i p =>
match get i hyps with
PSome (
A //\\ B) =>
check_proof (
hyps \ A \ B)
gl p
|
_=>
false
end
|
D_And i p =>
match get i hyps with
PSome (
A //\\ B =>> C) =>
check_proof (
hyps \ A=>>B=>>C)
gl p
|
_=>
false
end
|
I_Or_l p =>
match gl with
(
A \\// B) =>
check_proof hyps A p
|
_ =>
false
end
|
I_Or_r p =>
match gl with
(
A \\// B) =>
check_proof hyps B p
|
_ =>
false
end
|
E_Or i p1 p2 =>
match get i hyps with
PSome (
A \\// B) =>
check_proof (
hyps \ A)
gl p1 && check_proof (
hyps \ B)
gl p2
|
_=>
false
end
|
D_Or i p =>
match get i hyps with
PSome (
A \\// B =>> C) =>
(
check_proof (
hyps \ A=>>C \ B=>>C)
gl p)
|
_=>
false
end
|
Cut A p1 p2 =>
check_proof hyps A p1 && check_proof (
hyps \ A)
gl p2
end.
Theorem interp_proof:
forall p hyps F gl,
check_proof hyps gl p = true -> interp_ctx hyps F [[gl]].
Theorem Reflect:
forall gl prf,
if check_proof empty gl prf then [[gl]] else True.
End with_env.