diff options
| author | Chantal Keller <Chantal.Keller@lri.fr> | 2021-02-23 18:29:59 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@lri.fr> | 2021-02-23 18:29:59 +0100 |
| commit | c05f39c2556725610840ec48b62243a10e2e098f (patch) | |
| tree | 9fbcf56613f8641fa4a0cfb9535a3115142d0aed /unit-tests | |
| parent | 240b76807340e59bb85b35e3ebbb807792459912 (diff) | |
| download | smtcoq-c05f39c2556725610840ec48b62243a10e2e098f.tar.gz smtcoq-c05f39c2556725610840ec48b62243a10e2e098f.zip | |
The examples on lists uses the true list type
Diffstat (limited to 'unit-tests')
| -rw-r--r-- | unit-tests/Tests_verit_tactics.v | 15 |
1 files changed, 5 insertions, 10 deletions
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v index 2121ba2..83acc45 100644 --- a/unit-tests/Tests_verit_tactics.v +++ b/unit-tests/Tests_verit_tactics.v @@ -1071,32 +1071,27 @@ End EqualityOnUninterpretedType3. Section AppliedPolymorphicTypes2. - Variable list : Type -> Type. - Variable append : forall A : Type, list A -> list A -> list A. - Arguments append {A} _ _. - Local Notation "l1 +++ l2" := (append l1 l2) (at level 60). - Variable B : Type. Variable HlB : CompDec (list B). Goal forall l1 l2 l3 l4 : list B, - l1 +++ (l2 +++ (l3 +++ l4)) = l1 +++ (l2 +++ (l3 +++ l4)). + l1 ++ (l2 ++ (l3 ++ l4)) = l1 ++ (l2 ++ (l3 ++ l4)). Proof. verit. Qed. Hypothesis append_assoc_B : - forall l1 l2 l3 : list B, eqb_of_compdec HlB (l1 +++ (l2 +++ l3)) ((l1 +++ l2) +++ l3) = true. + forall l1 l2 l3 : list B, eqb_of_compdec HlB (l1 ++ (l2 ++ l3)) ((l1 ++ l2) ++ l3) = true. (* TODO: make it possible to apply prop2bool to hypotheses *) (* Hypothesis append_assoc_B : *) - (* forall l1 l2 l3 : list B, l1 +++ (l2 +++ l3) = (l1 +++ l2) +++ l3. *) + (* forall l1 l2 l3 : list B, l1 ++ (l2 ++ l3) = (l1 ++ l2) ++ l3. *) (* The hypothesis is not used *) Goal forall l1 l2 l3 l4 : list B, - l1 +++ (l2 +++ (l3 +++ l4)) = l1 +++ (l2 +++ (l3 +++ l4)). + l1 ++ (l2 ++ (l3 ++ l4)) = l1 ++ (l2 ++ (l3 ++ l4)). Proof. verit append_assoc_B. Qed. (* The hypothesis is used *) Goal forall l1 l2 l3 l4 : list B, - l1 +++ (l2 +++ (l3 +++ l4)) = ((l1 +++ l2) +++ l3) +++ l4. + l1 ++ (l2 ++ (l3 ++ l4)) = ((l1 ++ l2) ++ l3) ++ l4. Proof. verit append_assoc_B. Qed. End AppliedPolymorphicTypes2. |