Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: Rtauto.v Sprache: Coq

Original von: Coq^©

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Export List.
Require Export Bintree.
Require Import Bool BinPos.

Declare ML Module "rtauto_plugin".

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.
induction m;simpl;destruct n;congruence ||
(intro e;apply f_equal;auto).
Qed.

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.
induction p;destruct q;simpl;clean.
intro h;generalize (pos_eq_refl _ _ h);congruence.
case_eq (form_eq p1 q1);clean.
intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
case_eq (form_eq p1 q1);clean.
intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
case_eq (form_eq p1 q1);clean.
intros e1 e2;generalize (IHp1 _ e1) (IHp2 _ e2);congruence.
Qed.

Arguments form_eq_refl [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).
induction F;intros A H;simpl;auto.
Qed.

Lemma compose1 :
forall hyps F (A B:Prop),
(A -> B) ->
(interp_ctx hyps F A) ->
(interp_ctx hyps F B).
induction F;intros A B H;simpl;auto.
apply IHF;auto.
Qed.

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).
induction F;intros A B C H;simpl;auto.
apply IHF;auto.
Qed.

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).
induction F;intros A B C D H;simpl;auto.
apply IHF;auto.
Qed.

Lemma weaken : forall hyps F f G,
(interp_ctx hyps F G) ->
(interp_ctx (hyps\f)  (F_push f hyps F) G).
induction F;simpl;intros;auto.
apply compose1 with ([[a]]-> G);auto.
Qed.

Theorem project_In : forall hyps F g,
In g hyps F ->
interp_ctx hyps F [[g]].
induction F;simpl.
contradiction.
intros g H;destruct H.
subst;apply compose0;simpl;trivial.
apply compose1 with [[g]];auto.
Qed.

Theorem project : forall hyps F p g,
get  p hyps = PSome g->
interp_ctx hyps F [[g]].
intros hyps F p g e; apply project_In.
apply get_In with p;assumption.
Qed.

Arguments project [hyps] F [p 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]].

induction p; intros hyps F gl.

- (* Axiom *)
  simpl;case_eq (get p hyps);clean.
  intros f nth_f e;rewrite <- (form_eq_refl e).
  apply project with p;trivial.

- (* Arrow_Intro *)
  destruct gl; clean.
  simpl; intros.
  change (interp_ctx (hyps\gl1)  (F_push gl1 hyps F) [[gl2]]).
  apply IHp; try constructor; trivial.

- (* Arrow_Elim *)
  simpl check_proof; case_eq (get p hyps); clean.
  intros f ef; case_eq (get p0 hyps); clean.
  intros f0 ef0; destruct f0; clean.
  case_eq (form_eq f f0_1); clean.
  simpl; intros e check_p1.
  generalize  (project  F ef) (project  F ef0)
              (IHp (hyps \ f0_2) (F_push f0_2 hyps F) gl check_p1);
    clear check_p1 IHp p p0 p1 ef ef0.
  simpl.
  apply compose3.
  rewrite (form_eq_refl e).
  auto.

- (* Arrow_Destruct *)
  simpl; case_eq (get p1 hyps); clean.
  intros f ef; destruct f; clean.
  destruct f1; clean.
  case_eq (check_proof (hyps \ f1_2 =>> f2 \ f1_1) f1_2 p2); clean.
  intros check_p1 check_p2.
  generalize (project F ef)
             (IHp1 (hyps \ f1_2 =>> f2 \ f1_1)
                   (F_push f1_1 (hyps \ f1_2 =>> f2)
                           (F_push (f1_2 =>> f2) hyps F)) f1_2 check_p1)
             (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2).
  simpl; apply compose3; auto.

- (* False_Elim *)
  simpl; case_eq (get p hyps); clean.
  intros f ef; destruct f; clean.
  intros _; generalize (project F ef).
  apply compose1; apply False_ind.

- (* And_Intro *)
  simpl; destruct gl; clean.
  case_eq (check_proof hyps gl1 p1); clean.
  intros Hp1 Hp2;generalize (IHp1 hyps F gl1 Hp1) (IHp2 hyps F gl2 Hp2).
  apply compose2 ; simpl; auto.

- (* And_Elim *)
  simpl; case_eq (get p hyps); clean.
  intros f ef; destruct f; clean.
  intro check_p;
    generalize  (project F ef)
                (IHp (hyps \ f1 \ f2) (F_push f2 (hyps \ f1) (F_push f1 hyps F)) gl check_p).
  simpl; apply compose2; intros [h1 h2]; auto.

- (* And_Destruct*)
  simpl; case_eq (get p hyps); clean.
  intros f ef; destruct f; clean.
  destruct f1; clean.
  intro H;
    generalize (project F ef)
               (IHp (hyps \ f1_1 =>> f1_2 =>> f2)
                    (F_push (f1_1 =>> f1_2 =>> f2) hyps F) gl H);
    clear H; simpl.
  apply compose2; auto.

- (* Or_Intro_left *)
  destruct gl; clean.
  intro Hp; generalize (IHp hyps F gl1 Hp).
  apply compose1; simpl; auto.

- (* Or_Intro_right *)
  destruct gl; clean.
  intro Hp; generalize (IHp hyps F gl2 Hp).
  apply compose1; simpl; auto.

- (* Or_elim *)
  simpl; case_eq (get p1 hyps); clean.
  intros f ef; destruct f; clean.
  case_eq (check_proof (hyps \ f1) gl p2); clean.
  intros check_p1 check_p2;
    generalize (project F ef)
               (IHp1 (hyps \ f1) (F_push f1 hyps F) gl check_p1)
               (IHp2 (hyps \ f2) (F_push f2 hyps F) gl check_p2);
    simpl; apply compose3; simpl; intro h; destruct h; auto.

- (* Or_Destruct *)
  simpl; case_eq (get p hyps); clean.
  intros f ef; destruct f; clean.
  destruct f1; clean.
  intro check_p0;
    generalize (project F ef)
               (IHp (hyps \ f1_1 =>> f2 \ f1_2 =>> f2)
                    (F_push (f1_2 =>> f2) (hyps \ f1_1 =>> f2)
                            (F_push (f1_1 =>> f2) hyps F)) gl check_p0);
    simpl.
  apply compose2; auto.

- (* Cut *)
  simpl; case_eq (check_proof hyps f p1); clean.
  intros check_p1 check_p2;
    generalize (IHp1 hyps F f check_p1)
               (IHp2 (hyps\f) (F_push f hyps F) gl check_p2);
    simpl; apply compose2; auto.
Qed.

Theorem Reflect: forall gl prf, if check_proof empty gl prf then [[gl]] else True.
intros gl prf;case_eq (check_proof empty gl prf);intro check_prf.
change (interp_ctx empty F_empty [[gl]]) ;
apply interp_proof with prf;assumption.
trivial.
Qed.

End with_env.

(*
(* A small example *)
Parameters A B C D:Prop.
Theorem toto:A /\ (B \/ C) -> (A /\ B) \/ (A /\ C).
exact (Reflect (empty \ A \ B \ C)
([1] //\\ ([2] \\// [3]) =>> [1] //\\ [2] \\// [1] //\\ [3])
(I_Arrow (E_And 1 (E_Or 3
  (I_Or_l (I_And (Ax 2) (Ax 4)))
  (I_Or_r (I_And (Ax 2) (Ax 4))))))).
Qed.
Print toto.
*)

Register Reflect as plugins.rtauto.Reflect.

Register Atom as plugins.rtauto.Atom.
Register Arrow as plugins.rtauto.Arrow.
Register Bot as plugins.rtauto.Bot.
Register Conjunct as plugins.rtauto.Conjunct.
Register Disjunct as plugins.rtauto.Disjunct.

Register Ax as plugins.rtauto.Ax.
Register I_Arrow as plugins.rtauto.I_Arrow.
Register E_Arrow as plugins.rtauto.E_Arrow.
Register D_Arrow as plugins.rtauto.D_Arrow.
Register E_False as plugins.rtauto.E_False.
Register I_And as plugins.rtauto.I_And.
Register E_And as plugins.rtauto.E_And.
Register D_And as plugins.rtauto.D_And.
Register I_Or_l as plugins.rtauto.I_Or_l.
Register I_Or_r as plugins.rtauto.I_Or_r.
Register E_Or as plugins.rtauto.E_Or.
Register D_Or as plugins.rtauto.D_Or.

¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.