diff options
Diffstat (limited to 'source/Render/Html.hs')
| -rw-r--r-- | source/Render/Html.hs | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/source/Render/Html.hs b/source/Render/Html.hs index 90bef42..a45f422 100644 --- a/source/Render/Html.hs +++ b/source/Render/Html.hs @@ -2112,6 +2112,15 @@ elementOfFormula :: Expr -> Expr -> Formula elementOfFormula left right = FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere ElementSymbol []) (right :| [])) +semanticSubsetFormula :: Set VarSymbol -> Expr -> Expr -> Formula +semanticSubsetFormula reserved left right = + forallIfNeeded [witnessVar] + (impliesFormula + (elementOfFormula (ExprVar witnessVar) left) + (elementOfFormula (ExprVar witnessVar) right)) + where + witnessVar = freshDatatypeVar (reserved <> Set.fromList (exprVars left <> exprVars right)) "x" + equalsFormula :: Expr -> Expr -> Formula equalsFormula left right = FormulaChain (ChainBase (left :| []) Positive (Relation Nowhere EqSymbol []) (right :| [])) @@ -2331,7 +2340,7 @@ inductiveIntroFormula info clause = inductiveDomSubsetFormula :: InductiveRenderInfo -> Formula inductiveDomSubsetFormula info = forallIfNeeded (inductiveRenderParams info) - (FormulaChain (ChainBase (inductiveRenderCarrierExpr info :| []) Positive (Relation Nowhere SubseteqSymbol []) (inductiveRenderDomainExpr info :| []))) + (semanticSubsetFormula (inductiveUsedVars info) (inductiveRenderCarrierExpr info) (inductiveRenderDomainExpr info)) inductiveCasesFormula :: InductiveRenderInfo -> Formula inductiveCasesFormula info = @@ -2354,7 +2363,10 @@ inductiveInductFormula info = subsetVar = freshDatatypeVar (inductiveUsedVars info) "S" closures = inductiveInductionClosure subsetVar <$> NonEmpty.toList (inductiveRenderClauses info) conclusion = - FormulaChain (ChainBase (inductiveRenderCarrierExpr info :| []) Positive (Relation Nowhere SubseteqSymbol []) (ExprVar subsetVar :| [])) + semanticSubsetFormula + (Set.insert subsetVar (inductiveUsedVars info)) + (inductiveRenderCarrierExpr info) + (ExprVar subsetVar) inductiveInductionClosure :: VarSymbol -> InductiveRenderClause -> Formula inductiveInductionClosure subsetVar clause = |