diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 23:46:10 +0200 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2016-04-26 23:46:10 +0200 |
| commit | 3fac4bd6183b19e7980d9e0131dffa7a49f4c096 (patch) | |
| tree | 626ed0a12332262a8506cd56a5d31e00aea321cb /src | |
| parent | a5bd782f300c3767936fc3f45df6a09cda185370 (diff) | |
| download | smtcoq-3fac4bd6183b19e7980d9e0131dffa7a49f4c096.tar.gz smtcoq-3fac4bd6183b19e7980d9e0131dffa7a49f4c096.zip | |
The tactic "verit" generates more user-friendly subgoals
Diffstat (limited to 'src')
| -rw-r--r-- | src/SMT_terms.v | 12 | ||||
| -rw-r--r-- | src/trace/coqTerms.ml | 4 | ||||
| -rw-r--r-- | src/trace/smtAtom.ml | 25 |
3 files changed, 19 insertions, 22 deletions
diff --git a/src/SMT_terms.v b/src/SMT_terms.v index 6c5ba27..daca0f2 100644 --- a/src/SMT_terms.v +++ b/src/SMT_terms.v @@ -237,16 +237,10 @@ Record typ_eqb : Type := Typ_eqb { Section Typ_eqb_param. Variable A : Type. + Variable r : { eq : A -> A -> bool & forall x y, reflect (x = y) (eq x y) }. - Record typ_eqb_param : Type := Typ_eqb_param { - te_eqb_param : A -> A -> bool; - te_reflect_param : forall x y, reflect (x = y) (te_eqb_param x y) - }. - - Variable r : typ_eqb_param. - - Definition typ_eqb_of_typ_eqb_param := - Typ_eqb A (te_eqb_param r) (te_reflect_param r). + Definition typ_eqb_of_typ_eqb_param : typ_eqb := + Typ_eqb A (projT1 r) (projT2 r). End Typ_eqb_param. diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml index 1cc6d4f..429ed72 100644 --- a/src/trace/coqTerms.ml +++ b/src/trace/coqTerms.ml @@ -85,6 +85,9 @@ let cNone = gen_constant init_modules "None" (* Pairs *) let cpair = gen_constant init_modules "pair" +(* Dependent pairs *) +let csigT = gen_constant init_modules "sigT" + (* Logical Operators *) let cnot = gen_constant init_modules "not" let ceq = gen_constant init_modules "eq" @@ -112,7 +115,6 @@ let ctyp_eqb = gen_constant smt_modules "typ_eqb" let cTyp_eqb = gen_constant smt_modules "Typ_eqb" let cte_carrier = gen_constant smt_modules "te_carrier" let cte_eqb = gen_constant smt_modules "te_eqb" -let ctyp_eqb_param = gen_constant smt_modules "typ_eqb_param" let ctyp_eqb_of_typ_eqb_param = gen_constant smt_modules "typ_eqb_of_typ_eqb_param" let cunit_typ_eqb = gen_constant smt_modules "unit_typ_eqb" diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml index bbad580..979e4e4 100644 --- a/src/trace/smtAtom.ml +++ b/src/trace/smtAtom.ml @@ -92,18 +92,19 @@ module Btype = let eq_name = Names.id_of_string ("eq"^n) in let eq_var = Term.mkVar eq_name in - (* let eq_ty = Term.mkArrow t (Term.mkArrow t (Lazy.force cbool)) in *) - - (* let eq = mkName "eq" in *) - (* let x = mkName "x" in *) - (* let y = mkName "y" in *) - (* let req = Term.mkRel 3 in *) - (* let rx = Term.mkRel 2 in *) - (* let ry = Term.mkRel 1 in *) - (* let eq_refl_ty = Term.mkLambda (eq, eq_ty, Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|]; Term.mkApp (req, [|rx;ry|])|]))) in *) - - let eq_ty = mklApp ctyp_eqb_param [|t|] in - reify.cuts <- (eq_name, eq_ty)::reify.cuts; + let eq_ty = Term.mkArrow t (Term.mkArrow t (Lazy.force cbool)) in + + let eq = mkName "eq" in + let x = mkName "x" in + let y = mkName "y" in + let req = Term.mkRel 3 in + let rx = Term.mkRel 2 in + let ry = Term.mkRel 1 in + let refl_ty = Term.mkLambda (eq, eq_ty, Term.mkProd (x,t,Term.mkProd (y,t,mklApp creflect [|mklApp ceq [|t;rx;ry|]; Term.mkApp (req, [|rx;ry|])|]))) in + + let pair_ty = mklApp csigT [|eq_ty; refl_ty|] in + + reify.cuts <- (eq_name, pair_ty)::reify.cuts; let ce = mklApp ctyp_eqb_of_typ_eqb_param [|t; eq_var|] in declare reify t ce |